From 688a0869f6b8ab3048a545f821f45bc5599ba63b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Apr 2020 20:22:13 -0400 Subject: [hints] Move and split Hint Declaration AST to vernac This moves the vernacular part of hints to `vernac`; in particular, it helps removing the declaration of constants as parts of the `tactic` folder. --- plugins/ltac/g_ltac.mlg | 2 +- tactics/hints.ml | 125 -------------------------------- tactics/hints.mli | 18 ----- vernac/.ocamlformat-enable | 1 + vernac/classes.mli | 10 +-- vernac/comHints.ml | 174 +++++++++++++++++++++++++++++++++++++++++++++ vernac/comHints.mli | 29 ++++++++ vernac/g_proofs.mlg | 1 + vernac/ppvernac.ml | 3 +- vernac/pvernac.mli | 2 +- vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 2 +- vernac/vernacexpr.ml | 8 +-- 13 files changed, 220 insertions(+), 156 deletions(-) create mode 100644 vernac/.ocamlformat-enable create mode 100644 vernac/comHints.ml create mode 100644 vernac/comHints.mli diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg index e713ab13b2..5baa23b3e9 100644 --- a/plugins/ltac/g_ltac.mlg +++ b/plugins/ltac/g_ltac.mlg @@ -342,7 +342,7 @@ GRAMMAR EXTEND Gram hint: [ [ IDENT "Extern"; n = natural; c = OPT Constr.constr_pattern ; "=>"; tac = Pltac.tactic -> - { Hints.HintsExtern (n,c, in_tac tac) } ] ] + { ComHints.HintsExtern (n,c, in_tac tac) } ] ] ; operconstr: LEVEL "0" [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" -> diff --git a/tactics/hints.ml b/tactics/hints.ml index ffb0e030db..0499ba200e 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -23,7 +23,6 @@ open Globnames open Libobject open Namegen open Libnames -open Smartlocate open Termops open Inductiveops open Typeclasses @@ -100,8 +99,6 @@ let empty_hint_info = (* The Type of Constructions Autotactic Hints *) (************************************************************************) -type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen - type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -164,10 +161,6 @@ type full_hint = hint with_metadata type hint_entry = GlobRef.t option * raw_hint hint_ast with_uid with_metadata -type reference_or_constr = - | HintsReference of qualid - | HintsConstr of Constrexpr.constr_expr - type hint_mode = | ModeInput (* No evars *) | ModeNoHeadEvar (* No evar at the head *) @@ -178,16 +171,6 @@ type 'a hints_transparency_target = | HintsConstants | HintsReferences of 'a list -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of qualid list - | HintsTransparency of qualid hints_transparency_target * bool - | HintsMode of qualid * hint_mode list - | HintsConstructors of qualid list - | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - type import_level = HintLax | HintWarn | HintStrict let warn_hint_to_string = function @@ -1310,114 +1293,6 @@ let prepare_hint check env init (sigma,c) = let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in (c', diff) -let project_hint ~poly pri l2r r = - let open EConstr in - let open Coqlib in - let gr = Smartlocate.global_with_alias r in - let env = Global.env() in - let sigma = Evd.from_env env in - let sigma, c = Evd.fresh_global env sigma gr in - let t = Retyping.get_type_of env sigma c in - let t = - Tacred.reduce_to_quantified_ref env sigma (lib_ref "core.iff.type") t in - let sign,ccl = decompose_prod_assum sigma t in - let (a,b) = match snd (decompose_app sigma ccl) with - | [a;b] -> (a,b) - | _ -> assert false in - let p = - if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in - let sigma, p = Evd.fresh_global env sigma p in - let c = Reductionops.whd_beta sigma (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) in - let c = it_mkLambda_or_LetIn - (mkApp (p,[|mkArrow a Sorts.Relevant (lift 1 b);mkArrow b Sorts.Relevant (lift 1 a);c|])) sign in - let name = - Nameops.add_suffix (Nametab.basename_of_global gr) ("_proj_" ^ (if l2r then "l2r" else "r2l")) - in - let ctx = Evd.univ_entry ~poly sigma in - let c = EConstr.to_constr sigma c in - let cb = Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) in - let c = Declare.declare_constant - ~local:Declare.ImportDefaultBehavior - ~name ~kind:Decls.(IsDefinition Definition) cb - in - let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in - (info,false,true,PathAny, IsGlobRef (GlobRef.ConstRef c)) - -let warn_deprecated_hint_constr = - CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" - (fun () -> - Pp.strbrk - "Declaring arbitrary terms as hints is deprecated; declare a global reference instead" - ) - -let interp_hints ~poly = - fun h -> - let env = Global.env () in - let sigma = Evd.from_env env in - let f poly c = - let evd,c = Constrintern.interp_open_constr env sigma c in - let env = Global.env () in - let sigma = Evd.from_env env in - let (c, diff) = prepare_hint true env sigma (evd,c) in - if poly then IsConstr (c, diff) - else - let () = Declare.declare_universe_context ~poly:false diff in - IsConstr (c, Univ.ContextSet.empty) - in - let fref r = - let gr = global_with_alias r in - Dumpglob.add_glob ?loc:r.CAst.loc gr; - gr in - let fr r = evaluable_of_global_reference env (fref r) in - let fi c = - match c with - | HintsReference c -> - let gr = global_with_alias c in - (PathHints [gr], poly, IsGlobRef gr) - | HintsConstr c -> - let () = warn_deprecated_hint_constr () in - (PathAny, poly, f poly c) - in - let fp = Constrintern.intern_constr_pattern env sigma in - let fres (info, b, r) = - let path, poly, gr = fi r in - let info = { info with hint_pattern = Option.map fp info.hint_pattern } in - (info, poly, b, path, gr) - in - let ft = function - | HintsVariables -> HintsVariables - | HintsConstants -> HintsConstants - | HintsReferences lhints -> HintsReferences (List.map fr lhints) - in - let fp = Constrintern.intern_constr_pattern (Global.env()) in - match h with - | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) - | HintsResolveIFF (l2r, lc, n) -> - HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) - | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) - | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) - | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b) - | HintsMode (r, l) -> HintsModeEntry (fref r, l) - | HintsConstructors lqid -> - let constr_hints_of_ind qid = - let ind = global_inductive_with_alias qid in - let mib,_ = Global.lookup_inductive ind in - Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" (string_of_qualid qid) "ind"; - List.init (nconstructors env ind) - (fun i -> let c = (ind,i+1) in - let gr = GlobRef.ConstructRef c in - empty_hint_info, - (Declareops.inductive_is_polymorphic mib), true, - PathHints [gr], IsGlobRef gr) - in HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) - | HintsExtern (pri, patcom, tacexp) -> - let pat = Option.map (fp sigma) patcom in - let l = match pat with None -> [] | Some (l, _) -> l in - let ltacvars = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty l in - let env = Genintern.({ (empty_glob_sign env) with ltacvars }) in - let _, tacexp = Genintern.generic_intern env tacexp in - HintsExternEntry ({ hint_priority = Some pri; hint_pattern = pat }, tacexp) - let add_hints ~locality dbnames h = let local, superglobal = match locality with | Goptions.OptDefault | Goptions.OptGlobal -> false, true diff --git a/tactics/hints.mli b/tactics/hints.mli index eed0e37fac..a54da8ef0a 100644 --- a/tactics/hints.mli +++ b/tactics/hints.mli @@ -32,8 +32,6 @@ val empty_hint_info : 'a Typeclasses.hint_info_gen (** Pre-created hint databases *) -type hint_info_expr = Constrexpr.constr_pattern_expr hint_info_gen - type 'a hint_ast = | Res_pf of 'a (* Hint Apply *) | ERes_pf of 'a (* Hint EApply *) @@ -78,10 +76,6 @@ type search_entry type hint_entry -type reference_or_constr = - | HintsReference of Libnames.qualid - | HintsConstr of Constrexpr.constr_expr - type hint_mode = | ModeInput (* No evars *) | ModeNoHeadEvar (* No evar at the head *) @@ -92,16 +86,6 @@ type 'a hints_transparency_target = | HintsConstants | HintsReferences of 'a list -type hints_expr = - | HintsResolve of (hint_info_expr * bool * reference_or_constr) list - | HintsResolveIFF of bool * Libnames.qualid list * int option - | HintsImmediate of reference_or_constr list - | HintsUnfold of Libnames.qualid list - | HintsTransparency of Libnames.qualid hints_transparency_target * bool - | HintsMode of Libnames.qualid * hint_mode list - | HintsConstructors of Libnames.qualid list - | HintsExtern of int * Constrexpr.constr_expr option * Genarg.raw_generic_argument - type 'a hints_path_gen = | PathAtom of 'a hints_path_atom_gen | PathStar of 'a hints_path_gen @@ -217,8 +201,6 @@ val current_db_names : unit -> String.Set.t val current_pure_db : unit -> hint_db list -val interp_hints : poly:bool -> hints_expr -> hints_entry - val add_hints : locality:Goptions.option_locality -> hint_db_name list -> hints_entry -> unit val prepare_hint : bool (* Check no remaining evars *) -> diff --git a/vernac/.ocamlformat-enable b/vernac/.ocamlformat-enable new file mode 100644 index 0000000000..ffaa7e70f4 --- /dev/null +++ b/vernac/.ocamlformat-enable @@ -0,0 +1 @@ +comHints.ml diff --git a/vernac/classes.mli b/vernac/classes.mli index 9698c14452..f410cddfef 100644 --- a/vernac/classes.mli +++ b/vernac/classes.mli @@ -22,7 +22,7 @@ val declare_instance : ?warn:bool -> env -> Evd.evar_map -> Does nothing — or emit a “not-a-class” warning if the [warn] argument is set — when said type is not a registered type class. *) -val existing_instance : bool -> qualid -> Hints.hint_info_expr option -> unit +val existing_instance : bool -> qualid -> ComHints.hint_info_expr option -> unit (** globality, reference, optional priority and pattern information *) val new_instance_interactive @@ -34,7 +34,7 @@ val new_instance_interactive -> ?generalize:bool -> ?tac:unit Proofview.tactic -> ?hook:(GlobRef.t -> unit) - -> Hints.hint_info_expr + -> ComHints.hint_info_expr -> (bool * constr_expr) option -> Id.t * Lemmas.t @@ -47,7 +47,7 @@ val new_instance -> (bool * constr_expr) -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) - -> Hints.hint_info_expr + -> ComHints.hint_info_expr -> Id.t val new_instance_program @@ -59,7 +59,7 @@ val new_instance_program -> (bool * constr_expr) option -> ?generalize:bool -> ?hook:(GlobRef.t -> unit) - -> Hints.hint_info_expr + -> ComHints.hint_info_expr -> Id.t val declare_new_instance @@ -69,7 +69,7 @@ val declare_new_instance -> ident_decl -> local_binder_expr list -> constr_expr - -> Hints.hint_info_expr + -> ComHints.hint_info_expr -> unit (** {6 Low level interface used by Add Morphism, do not use } *) diff --git a/vernac/comHints.ml b/vernac/comHints.ml new file mode 100644 index 0000000000..324fee72ec --- /dev/null +++ b/vernac/comHints.ml @@ -0,0 +1,174 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* (a, b) + | _ -> assert false + in + let p = if l2r then lib_ref "core.iff.proj1" else lib_ref "core.iff.proj2" in + let sigma, p = Evd.fresh_global env sigma p in + let c = + Reductionops.whd_beta sigma + (mkApp (c, Context.Rel.to_extended_vect mkRel 0 sign)) + in + let c = + it_mkLambda_or_LetIn + (mkApp + ( p + , [| mkArrow a Sorts.Relevant (Vars.lift 1 b) + ; mkArrow b Sorts.Relevant (Vars.lift 1 a) + ; c |] )) + sign + in + let name = + Nameops.add_suffix + (Nametab.basename_of_global gr) + ("_proj_" ^ if l2r then "l2r" else "r2l") + in + let ctx = Evd.univ_entry ~poly sigma in + let c = EConstr.to_constr sigma c in + let cb = + Declare.(DefinitionEntry (definition_entry ~univs:ctx ~opaque:false c)) + in + let c = + Declare.declare_constant ~local:Declare.ImportDefaultBehavior ~name + ~kind:Decls.(IsDefinition Definition) + cb + in + let info = {Typeclasses.hint_priority = pri; hint_pattern = None} in + (info, false, true, Hints.PathAny, Hints.IsGlobRef (Names.GlobRef.ConstRef c)) + +let warn_deprecated_hint_constr = + CWarnings.create ~name:"deprecated-hint-constr" ~category:"deprecated" + (fun () -> + Pp.strbrk + "Declaring arbitrary terms as hints is deprecated; declare a global \ + reference instead") + +let interp_hints ~poly h = + let env = Global.env () in + let sigma = Evd.from_env env in + let f poly c = + let evd, c = Constrintern.interp_open_constr env sigma c in + let env = Global.env () in + let sigma = Evd.from_env env in + let c, diff = Hints.prepare_hint true env sigma (evd, c) in + if poly then (Hints.IsConstr (c, diff) [@ocaml.warning "-3"]) + else + let () = Declare.declare_universe_context ~poly:false diff in + (Hints.IsConstr (c, Univ.ContextSet.empty) [@ocaml.warning "-3"]) + in + let fref r = + let gr = Smartlocate.global_with_alias r in + Dumpglob.add_glob ?loc:r.CAst.loc gr; + gr + in + let fr r = Tacred.evaluable_of_global_reference env (fref r) in + let fi c = + let open Hints in + match c with + | HintsReference c -> + let gr = Smartlocate.global_with_alias c in + (PathHints [gr], poly, IsGlobRef gr) + | HintsConstr c -> + let () = warn_deprecated_hint_constr () in + (PathAny, poly, f poly c) + in + let fp = Constrintern.intern_constr_pattern env sigma in + let fres (info, b, r) = + let path, poly, gr = fi r in + let info = + { info with + Typeclasses.hint_pattern = Option.map fp info.Typeclasses.hint_pattern + } + in + (info, poly, b, path, gr) + in + let ft = + let open Hints in + function + | HintsVariables -> HintsVariables + | HintsConstants -> HintsConstants + | HintsReferences lhints -> HintsReferences (List.map fr lhints) + in + let fp = Constrintern.intern_constr_pattern (Global.env ()) in + let open Hints in + match h with + | HintsResolve lhints -> HintsResolveEntry (List.map fres lhints) + | HintsResolveIFF (l2r, lc, n) -> + HintsResolveEntry (List.map (project_hint ~poly n l2r) lc) + | HintsImmediate lhints -> HintsImmediateEntry (List.map fi lhints) + | HintsUnfold lhints -> HintsUnfoldEntry (List.map fr lhints) + | HintsTransparency (t, b) -> HintsTransparencyEntry (ft t, b) + | HintsMode (r, l) -> HintsModeEntry (fref r, l) + | HintsConstructors lqid -> + let constr_hints_of_ind qid = + let ind = Smartlocate.global_inductive_with_alias qid in + let mib, _ = Global.lookup_inductive ind in + Dumpglob.dump_reference ?loc:qid.CAst.loc "<>" + (Libnames.string_of_qualid qid) + "ind"; + List.init (Inductiveops.nconstructors env ind) (fun i -> + let c = (ind, i + 1) in + let gr = Names.GlobRef.ConstructRef c in + ( empty_hint_info + , Declareops.inductive_is_polymorphic mib + , true + , PathHints [gr] + , IsGlobRef gr )) + in + HintsResolveEntry (List.flatten (List.map constr_hints_of_ind lqid)) + | HintsExtern (pri, patcom, tacexp) -> + let pat = Option.map (fp sigma) patcom in + let l = match pat with None -> [] | Some (l, _) -> l in + let ltacvars = + List.fold_left + (fun accu x -> Names.Id.Set.add x accu) + Names.Id.Set.empty l + in + let env = Genintern.{(empty_glob_sign env) with ltacvars} in + let _, tacexp = Genintern.generic_intern env tacexp in + HintsExternEntry + ({Typeclasses.hint_priority = Some pri; hint_pattern = pat}, tacexp) diff --git a/vernac/comHints.mli b/vernac/comHints.mli new file mode 100644 index 0000000000..77fbef5387 --- /dev/null +++ b/vernac/comHints.mli @@ -0,0 +1,29 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(* hints_expr -> Hints.hints_entry diff --git a/vernac/g_proofs.mlg b/vernac/g_proofs.mlg index 058fa691ee..e84fce5504 100644 --- a/vernac/g_proofs.mlg +++ b/vernac/g_proofs.mlg @@ -14,6 +14,7 @@ open Glob_term open Constrexpr open Vernacexpr open Hints +open ComHints open Pcoq open Pcoq.Prim diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 36d79bfdb1..f1aae239aa 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -185,7 +185,7 @@ open Pputils | [] -> mt() | _ as z -> str":" ++ spc() ++ prlist_with_sep sep str z - let pr_reference_or_constr pr_c = let open Hints in function + let pr_reference_or_constr pr_c = let open ComHints in function | HintsReference r -> pr_qualid r | HintsConstr c -> pr_c c @@ -202,6 +202,7 @@ open Pputils let opth = pr_opt_hintbases db in let pph = let open Hints in + let open ComHints in match h with | HintsResolve l -> keyword "Resolve " ++ prlist_with_sep sep diff --git a/vernac/pvernac.mli b/vernac/pvernac.mli index 4de12f5e3b..2b6beaf2e3 100644 --- a/vernac/pvernac.mli +++ b/vernac/pvernac.mli @@ -28,7 +28,7 @@ module Vernac_ : val command_entry : vernac_expr Entry.t val main_entry : vernac_control option Entry.t val red_expr : raw_red_expr Entry.t - val hint_info : Hints.hint_info_expr Entry.t + val hint_info : ComHints.hint_info_expr Entry.t end (* To be removed when the parser is made functional wrt the tactic diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib index b7728fe699..3d3be8050d 100644 --- a/vernac/vernac.mllib +++ b/vernac/vernac.mllib @@ -9,6 +9,7 @@ Himsg Locality Egramml Vernacextend +ComHints Ppvernac Proof_using Egramcoq diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 3926b91a55..028a7d0859 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -1275,7 +1275,7 @@ let vernac_hints ~atts dbnames h = "This command does not support the export attribute in sections."); | OptDefault | OptLocal -> () in - Hints.add_hints ~locality dbnames (Hints.interp_hints ~poly h) + Hints.add_hints ~locality dbnames (ComHints.interp_hints ~poly h) let vernac_syntactic_definition ~atts lid x only_parsing = let module_local, deprecation = Attributes.(parse Notations.(module_locality ++ deprecation) atts) in diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml index e46186288e..b65a0da1cc 100644 --- a/vernac/vernacexpr.ml +++ b/vernac/vernacexpr.ml @@ -336,18 +336,18 @@ type nonrec vernac_expr = local_binder_expr list * (* binders *) constr_expr * (* type *) (bool * constr_expr) option * (* body (bool=true when using {}) *) - Hints.hint_info_expr + ComHints.hint_info_expr | VernacDeclareInstance of ident_decl * (* name *) local_binder_expr list * (* binders *) constr_expr * (* type *) - Hints.hint_info_expr + ComHints.hint_info_expr | VernacContext of local_binder_expr list | VernacExistingInstance of - (qualid * Hints.hint_info_expr) list (* instances names, priorities and patterns *) + (qualid * ComHints.hint_info_expr) list (* instances names, priorities and patterns *) | VernacExistingClass of qualid (* inductive or definition name *) @@ -387,7 +387,7 @@ type nonrec vernac_expr = (* Commands *) | VernacCreateHintDb of string * bool | VernacRemoveHints of string list * qualid list - | VernacHints of string list * Hints.hints_expr + | VernacHints of string list * ComHints.hints_expr | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) * onlyparsing_flag -- cgit v1.2.3 From e04377e2c5eca2b47bd5f8db320069aa47040488 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sat, 18 Apr 2020 22:58:40 -0400 Subject: [declare] [tactics] Move declare to `vernac` This PR moves `Declare` to `vernac` which will hopefully allow to unify it with `DeclareDef` and avoid exposing entry internals. There are many tradeoffs to be made as interface and placement of tactics is far from clear; I've tried to reach a minimally invasive compromise: - moved leminv to `ltac_plugin`; this is unused in the core codebase and IMO for now it is the best place - hook added for abstract; this should be cleaned up later - hook added for scheme declaration; this should be cleaned up later - separation of hints vernacular and "tactic" part should be also done later, for now I've introduced a `declareUctx` module to avoid being invasive there. In particular this last point strongly suggest that for now, the best place for `Class_tactics` would be also in `ltac`, but I've avoided that for now too. This partially supersedes #10951 for now and helps with #11492 . --- dev/base_include | 2 +- plugins/ltac/extratactics.mlg | 2 +- plugins/ltac/leminv.ml | 297 +++++++++++++ plugins/ltac/leminv.mli | 21 + plugins/ltac/ltac_plugin.mlpack | 1 + plugins/setoid_ring/newring.ml | 2 +- tactics/abstract.ml | 5 +- tactics/abstract.mli | 12 + tactics/declare.ml | 901 ---------------------------------------- tactics/declare.mli | 314 -------------- tactics/declareUctx.ml | 34 ++ tactics/declareUctx.mli | 11 + tactics/hints.ml | 5 +- tactics/hints.mli | 2 +- tactics/ind_tables.ml | 8 +- tactics/ind_tables.mli | 8 + tactics/leminv.ml | 297 ------------- tactics/leminv.mli | 21 - tactics/tactics.mllib | 3 +- vernac/comAssumption.ml | 6 +- vernac/comHints.ml | 2 +- vernac/declare.ml | 886 +++++++++++++++++++++++++++++++++++++++ vernac/declare.mli | 299 +++++++++++++ vernac/declareUniv.ml | 4 +- vernac/vernac.mllib | 1 + vernac/vernacentries.ml | 3 +- 26 files changed, 1593 insertions(+), 1554 deletions(-) create mode 100644 plugins/ltac/leminv.ml create mode 100644 plugins/ltac/leminv.mli delete mode 100644 tactics/declare.ml delete mode 100644 tactics/declare.mli create mode 100644 tactics/declareUctx.ml create mode 100644 tactics/declareUctx.mli delete mode 100644 tactics/leminv.ml delete mode 100644 tactics/leminv.mli create mode 100644 vernac/declare.ml create mode 100644 vernac/declare.mli diff --git a/dev/base_include b/dev/base_include index 96a867475d..45e79147c1 100644 --- a/dev/base_include +++ b/dev/base_include @@ -129,7 +129,7 @@ open Elim open Equality open Hipattern open Inv -open Leminv +open Ltac_plugin.Leminv open Tacticals open Tactics open Eqschemes diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg index 7754fe401e..0bad3cbe5b 100644 --- a/plugins/ltac/extratactics.mlg +++ b/plugins/ltac/extratactics.mlg @@ -312,7 +312,7 @@ let add_rewrite_hint ~poly bases ort t lcsr = if poly then ctx else (* This is a global universe context that shouldn't be refreshed at every use of the hint, declare it globally. *) - (Declare.declare_universe_context ~poly:false ctx; + (DeclareUctx.declare_universe_context ~poly:false ctx; Univ.ContextSet.empty) in CAst.make ?loc:(Constrexpr_ops.constr_loc ce) ((c, ctx), ort, Option.map (in_gen (rawwit wit_ltac)) t) in diff --git a/plugins/ltac/leminv.ml b/plugins/ltac/leminv.ml new file mode 100644 index 0000000000..5a8ec404ee --- /dev/null +++ b/plugins/ltac/leminv.ml @@ -0,0 +1,297 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * Copyright INRIA, CNRS and contributors *) +(*