diff --git a/doc/changelog/04-tactics/22192-noforce-scheme-Removed.rst b/doc/changelog/04-tactics/22192-noforce-scheme-Removed.rst new file mode 100644 index 000000000000..2a5b9477767a --- /dev/null +++ b/doc/changelog/04-tactics/22192-noforce-scheme-Removed.rst @@ -0,0 +1,4 @@ +- **Removed:** + automatic scheme generation by :tacn:`rewrite` + (`#22192 `_, + by Gaëtan Gilbert). diff --git a/engine/evd.ml b/engine/evd.ml index 85d325801689..83bc837c0ede 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -356,15 +356,11 @@ type evar_flags = rewrite_rule_evars : Evar.Set.t; } -type side_effect_role = -| Schema of inductive * string - type side_effects = { seff_safeenv : Safe_typing.safe_environment option; (* If seff_safeenv = Some senv, then senv = Global.safe_env + seff_private *) seff_labels : Id.Set.t; seff_private : Safe_typing.private_constants; - seff_roles : side_effect_role Cmap_env.t; seff_univs : UState.named_universes_entry Cmap_env.t; } @@ -871,7 +867,6 @@ let empty_side_effects = { seff_safeenv = None; seff_labels = Id.Set.empty; seff_private = Safe_typing.empty_private_constants; - seff_roles = Cmap_env.empty; seff_univs = Cmap_env.empty; } @@ -1259,7 +1254,6 @@ let concat_side_effects eff1 eff2 = { seff_safeenv = None; seff_labels = Id.Set.fold Id.Set.add eff1.seff_labels eff2.seff_labels; seff_private = Safe_typing.concat_private eff1.seff_private eff2.seff_private; - seff_roles = Cmap_env.fold Cmap_env.add eff1.seff_roles eff2.seff_roles; seff_univs = Cmap_env.fold Cmap_env.add eff1.seff_univs eff2.seff_univs; } @@ -1275,7 +1269,7 @@ let set_side_effects eff evd = let eval_side_effects evd = evd.effects -let push_side_effects ?role ?ts name de ctx effs = +let push_side_effects ?ts name de ctx effs = let senv = get_senv_side_effects effs in let senv = match ts with | None -> senv @@ -1287,14 +1281,9 @@ let push_side_effects ?role ?ts name de ctx effs = else Cmap_env.add kn (UState.Monomorphic_entry ctx, UnivNames.empty_binders) effs.seff_univs in - let seff_roles = match role with - | None -> effs.seff_roles - | Some r -> Cmap_env.add kn r effs.seff_roles - in let effs = { seff_private = Safe_typing.concat_private prv effs.seff_private; seff_labels = Id.Set.add (Constant.label kn) effs.seff_labels; - seff_roles = seff_roles; seff_univs = seff_univs; seff_safeenv = Some senv; } in @@ -1309,7 +1298,6 @@ let seff_mem_label id effs = Id.Set.mem id effs.seff_labels let seff_private eff = eff.seff_private -let seff_roles effs = effs.seff_roles let seff_univs effs = effs.seff_univs (* Future goals *) diff --git a/engine/evd.mli b/engine/evd.mli index d3dea4102c9a..70065dc57ceb 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -396,9 +396,6 @@ val dependent_evar_ident : Evar.t -> evar_map -> Id.t (** {5 Side-effects} *) -type side_effect_role = -| Schema of inductive * string - type side_effects val empty_side_effects : side_effects @@ -415,7 +412,7 @@ val eval_side_effects : evar_map -> side_effects (** Return the effects contained in the evar map. *) val push_side_effects : - ?role:side_effect_role -> ?ts:Conv_oracle.oracle -> + ?ts:Conv_oracle.oracle -> Id.t -> Safe_typing.side_effect_declaration -> Univ.ContextSet.t -> side_effects -> Constant.t * side_effects @@ -425,7 +422,6 @@ val avoid_side_effect_label : Id.t -> evar_map -> evar_map val seff_mem_label : Id.t -> side_effects -> bool val seff_private : side_effects -> Safe_typing.private_constants -val seff_roles : side_effects -> side_effect_role Cmap_env.t val seff_univs : side_effects -> UState.named_universes_entry Names.Cmap_env.t (** {5 Future goals} *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 885a1889dff8..76bbb7bbf149 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -467,41 +467,30 @@ let lookup_eq_eliminator_opt env sigma eq ~dep het_eq ~inccl l2r ~c_sort ~e_sort type eq_scheme_kind = Minimality of UnivGen.QualityOrSet.t | Rewriting | Equality -let warn_missing_scheme = CWarnings.create ~name:"missing-scheme" ~category:Deprecation.Version.v9_2 - Pp.(fun (kind,name,ind) -> - let ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) in - let cmd () = match kind with - | Minimality s -> - fmt "Scheme Minimality for %t Sort %t" - (const ind) (fun () -> UnivGen.QualityOrSet.raw_pr s) - | Rewriting -> fmt "Scheme Rewriting for %t" (const ind) - | Equality -> fmt "Scheme Equality for %t" (const ind) - in - hv 0 @@ fmt "Autogenerated \"%s\" scheme for %t.@ Use \"%t\" to explicitly generate it.@ This will become an error in the future." - name (const ind) cmd) - -let warn_missing_scheme = function - | None -> Proofview.tclUNIT() - | Some warn -> - Proofview.tclUNIT() >>= fun () -> - try warn_missing_scheme warn; Proofview.tclUNIT() - with e when CErrors.noncritical e -> - let e, info = Exninfo.capture e in - Proofview.tclZERO ~info e +exception MissingScheme of eq_scheme_kind * string * inductive + +let () = CErrors.register_handler @@ function + | MissingScheme (kind,name,ind) -> + let ind = Nametab.pr_global_env Id.Set.empty (IndRef ind) in + let cmd () = match kind with + | Minimality s -> + fmt "Scheme Minimality for %t Sort %t" + (const ind) (fun () -> UnivGen.QualityOrSet.raw_pr s) + | Rewriting -> fmt "Scheme Rewriting for %t" (const ind) + | Equality -> fmt "Scheme Equality for %t" (const ind) + in + let msg = hv 0 @@ fmt "Missing \"%s\" scheme for %t.@ Use \"%t\" to explicitly generate it.@ This will become an error in the future." + name (const ind) cmd + in + Some msg + | _ -> None (* find_elim determines which elimination principle is necessary to eliminate lbeq on sort_of_gl. *) let find_scheme kind scheme_name ind = - find_scheme scheme_name ind >>= function - | Some s -> Proofview.tclUNIT (s,None) - | None -> - force_find_scheme scheme_name ind >>= fun s -> - (* We delay the warning to avoid printing it if the rewrite - fails (compatible with the future behaviour where the missing - scheme is always error). Typically for [rewrite ?lem] where - [lem] is sometimes a proof of equality and sometimes not - rewriteable. *) - Proofview.tclUNIT (s, Some (kind, Ind_tables.scheme_kind_name scheme_name, ind)) + match lookup_scheme scheme_name ind with + | Some s -> Proofview.tclUNIT s + | None -> Proofview.tclZERO (MissingScheme (kind,Ind_tables.scheme_kind_name scheme_name,ind)) let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) = Proofview.Goal.enter_one begin fun gl -> @@ -510,10 +499,10 @@ let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) = let gen_elim () = match EConstr.kind sigma hdcncl with | Ind (ind,u) -> - find_scheme Rewriting (scheme_name dep lft2rgt inccl) ind >>= fun (elim,warn) -> + find_scheme Rewriting (scheme_name dep lft2rgt inccl) ind >>= fun elim -> Proofview.tclEVARMAP >>= fun sigma -> let (sigma, gref) = Evd.fresh_global env sigma elim in - Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (gref, UnknownPosition, warn) + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (gref, UnknownPosition) | _ -> assert false in let nb_args = List.length args in @@ -528,7 +517,7 @@ let find_elim lft2rgt dep inccl type_of_cls (ctx, hdcncl, args) = let p_sort = Retyping.get_sort_of env sigma type_of_cls in match lookup_eq_eliminator_opt env sigma hdcncl maybe_het_eq ~dep ~inccl lft2rgt ~c_sort ~e_sort ~p_sort with | Some ((sigma, c),indarg) -> - Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (c, indarg, None) + Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (c, indarg) | None -> gen_elim () else gen_elim () @@ -542,10 +531,9 @@ let leibniz_rewrite_ebindings_clause cls lft2rgt tac c ((_, hdcncl, _) as t) l w | Some id -> Tacmach.pf_get_hyp_typ id gl in let dep = dep_proof_ok && dependent_no_evar evd c type_of_cls in let inccl = Option.is_empty cls in - find_elim lft2rgt dep inccl type_of_cls t >>= fun (elim, indarg, warn) -> + find_elim lft2rgt dep inccl type_of_cls t >>= fun (elim, indarg) -> general_elim_clause with_evars frzevars tac cls c t l - lft2rgt elim indarg >>= fun () -> - warn_missing_scheme warn + lft2rgt elim indarg end let adjust_rewriting_direction args lft2rgt = @@ -1395,7 +1383,7 @@ let inject_if_homogenous_dependent_pair ty = | Some v -> v in let new_eq_args = [|Retyping.get_type_of env sigma ar1.(3);ar1.(3);ar2.(3)|] in - find_scheme Equality (!eq_dec_scheme_kind_name()) ind >>= fun (c, warn) -> + find_scheme Equality (!eq_dec_scheme_kind_name()) ind >>= fun c -> let sigma, c = fresh_global env sigma c in (* cut with the good equality and prove the requested goal *) tclTHENLIST @@ -1409,7 +1397,7 @@ let inject_if_homogenous_dependent_pair ty = Tactics.exact_check (mkApp(inj2,[|ar1.(0);c;ar1.(1);ar1.(2);ar1.(3);ar2.(3);hyp|])) ]); - warn_missing_scheme warn] + ] with Exit -> Proofview.tclUNIT () end diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index eed2ef3b0ed6..9c3b68c92ce2 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -24,12 +24,21 @@ open Util (**********************************************************************) (* Registering schemes in the environment *) -type handle = Evd.side_effects +type side_effect_role = +| Schema of inductive * string + +type schemes = { + sch_eff : Evd.side_effects; + sch_roles : side_effect_role Cmap_env.t; + sch_reg : (Id.t * Constant.t * Loc.t option * UState.named_universes_entry) list; +} + +type handle = schemes let push_handle eff = let open Proofview.Notations in Proofview.tclEVARMAP >>= fun sigma -> - let sigma = Evd.emit_side_effects eff sigma in + let sigma = Evd.emit_side_effects eff.sch_eff sigma in Proofview.Unsafe.tclEVARS sigma type mutual_scheme_object_function = @@ -97,7 +106,7 @@ let compute_name internal id avoid = Namegen.next_ident_away_from (add_prefix "internal_" id) visible else id -let declare_definition_scheme = ref (fun ~univs ~role ~name ~effs c -> +let declare_definition_scheme = ref (fun ~univs ~name ~effs c -> CErrors.anomaly (Pp.str "scheme declaration not registered")) let register_definition_scheme = ref (fun ~internal ~name ~const ~univs ?loc () -> @@ -106,19 +115,15 @@ let register_definition_scheme = ref (fun ~internal ~name ~const ~univs ?loc () let lookup_scheme kind ind = try Some (DeclareScheme.lookup_scheme kind (GlobRef.IndRef ind)) with Not_found -> None -type schemes = { - sch_eff : Evd.side_effects; - sch_reg : (Id.t * Constant.t * Loc.t option * UState.named_universes_entry) list; -} - let empty_schemes eff = { sch_eff = eff; sch_reg = []; + sch_roles = Cmap_env.empty; } -let redeclare_schemes { sch_eff = eff } = +let redeclare_schemes { sch_eff = eff; sch_roles = roles } = let fold c role accu = match role with - | Evd.Schema (ind, kind) -> + | Schema (ind, kind) -> try let _ = DeclareScheme.lookup_scheme kind (GlobRef.IndRef ind) in accu @@ -126,23 +131,24 @@ let redeclare_schemes { sch_eff = eff } = let old = try String.Map.find kind accu with Not_found -> [] in String.Map.add kind ((GlobRef.IndRef ind, GlobRef.ConstRef c) :: old) accu in - let schemes = Cmap_env.fold fold (Evd.seff_roles eff) String.Map.empty in + let schemes = Cmap_env.fold fold roles String.Map.empty in let iter kind defs = List.iter (DeclareScheme.declare_scheme SuperGlobal kind) defs in String.Map.iter iter schemes -let local_lookup_scheme eff kind ind = match lookup_scheme kind ind with +let local_lookup_scheme { sch_roles = roles } kind ind = + match lookup_scheme kind ind with | Some _ as ans -> ans | None -> let exception Found of Constant.t in let iter c role = match role with - | Evd.Schema (i, k) -> + | Schema (i, k) -> if String.equal k kind && Ind.UserOrd.equal i ind then raise (Found c) in (* Inefficient O(n), but the number of locally declared schemes is small and this is very rarely called *) - try let _ = Cmap_env.iter iter (Evd.seff_roles eff) in None with Found c -> Some (GlobRef.ConstRef c) + try let _ = Cmap_env.iter iter roles in None with Found c -> Some (GlobRef.ConstRef c) -let local_check_scheme kind ind { sch_eff = eff } = +let local_check_scheme kind ind eff = Option.has_some (local_lookup_scheme eff kind ind) let define ?loc internal role id c poly uctx sch = @@ -156,9 +162,10 @@ let define ?loc internal role id c poly uctx sch = let uctx = UState.restrict uctx (Vars.universes_of_constr c) in let univs = UState.univ_entry ~poly uctx in let effs = sch.sch_eff in - let cst, effs = !declare_definition_scheme ~univs ~role ~name:id ~effs c in + let cst, effs = !declare_definition_scheme ~univs ~name:id ~effs c in let reg = (id, cst, loc, univs) :: sch.sch_reg in - cst, { sch_eff = effs; sch_reg = reg } + let roles = Cmap_env.add cst role sch.sch_roles in + cst, { sch_eff = effs; sch_reg = reg; sch_roles = roles } module Locmap : sig @@ -209,12 +216,12 @@ let globally_declare_schemes sch = (* Assumes that dependencies are already defined *) let rec define_individual_scheme_base ?loc kind suff f ~internal idopt (mind,i as ind) eff = let env = get_env eff in - let (c, ctx) = f env eff.sch_eff ind in + let (c, ctx) = f env eff ind in let mib = Environ.lookup_mind mind env in let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename ("_"^suff) in - let role = Evd.Schema (ind, kind) in + let role = Schema (ind, kind) in let poly, cumulative = Declareops.inductive_is_polymorphic mib, Declareops.inductive_is_cumulative mib in let poly = PolyFlags.make ~univ_poly:poly ~cumulative ~collapse_sort_variables:true in let const, eff = define ?loc internal role id c poly ctx eff in @@ -233,13 +240,13 @@ and define_individual_scheme ?loc kind ~internal names (mind,i as ind) eff = (* Assumes that dependencies are already defined *) and define_mutual_scheme_base ?(locmap=Locmap.default None) kind suff f ~internal names mind eff = let env = get_env eff in - let (cl, ctx) = f env eff.sch_eff mind in + let (cl, ctx) = f env eff mind in let mib = Environ.lookup_mind mind env in let ids = Array.init (Array.length mib.mind_packets) (fun i -> try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename ("_"^suff)) in let fold i effs id cl = - let role = Evd.Schema ((mind, i), kind)in + let role = Schema ((mind, i), kind)in let loc = Locmap.lookup ~locmap (mind,i) in (* FIXME cumulativity not supported? *) let poly = PolyFlags.of_univ_poly (Declareops.inductive_is_polymorphic mib) in @@ -268,44 +275,6 @@ match sd with if local_check_scheme kind (mind, 0) eff then eff else define_mutual_scheme kind ~internal:true [] mind eff -let find_scheme kind (mind,i as ind) = - let open Proofview.Notations in - Proofview.tclEVARMAP >>= fun sigma -> - let s = local_lookup_scheme (Evd.eval_side_effects sigma) kind ind in - Proofview.tclUNIT s - -let force_find_scheme kind (mind,i as ind) = - let open Proofview.Notations in - Proofview.tclEVARMAP >>= fun sigma -> - let eff = Evd.eval_side_effects sigma in - match local_lookup_scheme eff kind ind with - | Some s -> - Proofview.tclUNIT s - | None -> - let senv = Evd.get_senv_side_effects eff in - try - let eff, ans = match Hashtbl.find scheme_object_table kind with - | s,IndividualSchemeFunction (f, deps) -> - let env = Safe_typing.env_of_safe_env senv in - let deps = match deps with None -> [] | Some deps -> deps env ind in - let sch = empty_schemes eff in - let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) sch deps in - let c, eff = define_individual_scheme_base kind s f ~internal:true None ind eff in - eff, c - | s,MutualSchemeFunction (f, deps) -> - let env = Safe_typing.env_of_safe_env senv in - let deps = match deps with None -> [] | Some deps -> deps env mind in - let sch = empty_schemes eff in - let eff = List.fold_left (fun eff dep -> declare_scheme_dependence eff dep) sch deps in - let ca, eff = define_mutual_scheme_base kind s f ~internal:true [] mind eff in - eff, ca.(i) - in - let sigma = Evd.emit_side_effects eff.sch_eff sigma in - Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclUNIT (GlobRef.ConstRef ans) - with Rocqlib.NotFoundRef _ as e -> - let e, info = Exninfo.capture e in - Proofview.tclZERO ~info e - let register_schemes sch = let iter (id, kn, loc, univs) = !register_definition_scheme ~internal:false ~name:id ~const:kn ~univs ?loc () diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 0c125e55b7fa..0a2c156b7b61 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -84,12 +84,6 @@ end val define_mutual_scheme : ?locmap:Locmap.t -> mutual scheme_kind -> (int * Id.t) list -> MutInd.t -> unit -(** Main function to retrieve a scheme in the cache *) -val find_scheme : 'a scheme_kind -> inductive -> GlobRef.t option Proofview.tactic - -(** Generates the scheme if not found *) -val force_find_scheme : 'a scheme_kind -> inductive -> GlobRef.t Proofview.tactic - (** Like [find_scheme] but does not generate a constant on the fly *) val lookup_scheme : 'a scheme_kind -> inductive -> GlobRef.t option @@ -100,7 +94,6 @@ val pr_scheme_kind : 'a scheme_kind -> Pp.t val declare_definition_scheme : (univs:UState.named_universes_entry - -> role:Evd.side_effect_role -> name:Id.t -> effs:Evd.side_effects -> Constr.t diff --git a/test-suite/bugs/bug_21304.v b/test-suite/bugs/bug_21304.v index a3891a769358..4038792e5d79 100644 --- a/test-suite/bugs/bug_21304.v +++ b/test-suite/bugs/bug_21304.v @@ -1,9 +1,8 @@ -(* NB this test can be removed once dynamic scheme declaration is removed - (ie when warning "missing-scheme" is replaced by an error) *) + Inductive equal T (x : T) : T -> Type := Equal : equal T x x. Lemma foo : forall a b, equal nat a b -> a = b. Proof. intros a b H. -rewrite <- H, H. +Fail rewrite <- H, H. Abort. diff --git a/test-suite/success/rewrite.v b/test-suite/success/rewrite.v index 643d677fb1d8..24530d0b6144 100644 --- a/test-suite/success/rewrite.v +++ b/test-suite/success/rewrite.v @@ -175,8 +175,7 @@ Proof. exact I. Qed. -(* test that "try rewrite" / "rewrite ?h" catches the error from mssing-scheme *) -Set Warnings "+missing-scheme". +(* test that "try rewrite" / "rewrite ?h" catches the error from missing-scheme *) Inductive myeq A x : A -> Prop := myrefl : myeq A x x. diff --git a/vernac/declare.ml b/vernac/declare.ml index c9060f33c560..54e04d1d050d 100644 --- a/vernac/declare.ml +++ b/vernac/declare.ml @@ -117,13 +117,13 @@ sig val make : Evd.side_effects -> t val concat : t -> t -> t val get : t -> Safe_typing.private_constants - val obj : t -> (Evd.side_effect_role option * UState.named_universes_entry option) Cmap_env.t + val obj : t -> (UState.named_universes_entry option) Cmap_env.t end = struct type t = { priv : Safe_typing.private_constants; - data : (Evd.side_effect_role option * UState.named_universes_entry option) Cmap_env.t; + data : (UState.named_universes_entry option) Cmap_env.t; } let empty = { @@ -133,9 +133,8 @@ let empty = { let make eff = let fold accu c = - let role = try Some (Cmap_env.find c (Evd.seff_roles eff)) with Not_found -> None in let univs = try Some (Cmap_env.find c (Evd.seff_univs eff)) with Not_found -> None in - Cmap_env.add c (role, univs) accu + Cmap_env.add c univs accu in let priv = Evd.seff_private eff in let data = List.fold_left fold Cmap_env.empty (Safe_typing.constants_of_private priv) in @@ -473,7 +472,7 @@ let register_constant loc cst kind ?user_warns local = Impargs.declare_constant_implicits cst; Notation.declare_ref_arguments_scope (GlobRef.ConstRef cst) -let register_side_effect (c, body, role, univs) = +let register_side_effect (c, body, univs) = (* Register the body in the opaque table *) let () = match body with | None -> () @@ -485,15 +484,13 @@ let register_side_effect (c, body, role, univs) = | None -> () | Some univs -> DeclareUniv.declare_univ_binders (ConstRef c) univs in - match role with - | None -> () - | Some (Evd.Schema (ind, kind)) -> DeclareScheme.declare_scheme SuperGlobal kind (GlobRef.IndRef ind, GlobRef.ConstRef c) + () -let get_roles export eff = +let get_univs export eff = let eff = SideEff.obj eff in let map (c, body) = - let role, univs = try (Cmap_env.find c eff) with Not_found -> None, None in - (c, body, role, univs) + let univs = try (Cmap_env.find c eff) with Not_found -> None in + (c, body, univs) in List.map map export @@ -501,7 +498,7 @@ let get_roles export eff = libobjects. *) let export_side_effects eff = let export = Global.export_private_constants (SideEff.get eff) in - let export = get_roles export eff in + let export = get_univs export eff in List.iter register_side_effect export (* This is different from [export_side_effects] as the former properly declares @@ -692,7 +689,7 @@ let declare_constant ~loc ?(local = Locality.ImportDefaultBehavior) ~name ~kind if unsafe || is_unsafe_typing_flags typing_flags then feedback_axiom(); kn -let declare_private_constant ?role ?ts ~name ~opaque de effs = +let declare_private_constant ?ts ~name ~opaque de effs = let de, ctx = if not opaque then let de, ctx = cast_pure_proof_entry de in @@ -702,7 +699,7 @@ let declare_private_constant ?role ?ts ~name ~opaque de effs = OpaqueEff de, ctx in - Evd.push_side_effects ?role ?ts name de ctx effs + Evd.push_side_effects ?ts name de ctx effs let inline_private_constants ~uctx env (body, eff) = let body, ctx = Safe_typing.inline_private_constants env (body, SideEff.get eff) in @@ -905,9 +902,9 @@ let process_proof ~info:Info.({ udecl; poly }) ?(is_telescope=false) = function ((body, uctx), eff)) in (delayed_definition_entry ?using ~univs ~types:initial_typ ~feedback_id body, initial_euctx)) -let declare_definition_scheme ~univs ~role ~name ~effs c = +let declare_definition_scheme ~univs ~name ~effs c = let entry = pure_definition_entry ~univs c in - declare_private_constant ~role ~name ~opaque:false entry effs + declare_private_constant ~name ~opaque:false entry effs let register_definition_scheme ~internal ~name ~const:kn ~univs ?loc () = let kind = Decls.(IsDefinition Scheme) in