aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/dune (renamed from plugins/ltac/plugin_base.dune)2
-rw-r--r--plugins/ltac/extratactics.mlg8
-rw-r--r--plugins/ltac/g_ltac.mlg16
-rw-r--r--plugins/ltac/rewrite.ml50
-rw-r--r--plugins/ltac/tacentries.ml2
-rw-r--r--plugins/ltac/tacenv.ml2
-rw-r--r--plugins/ltac/tacinterp.ml2
-rw-r--r--plugins/ltac/tactic_option.ml2
8 files changed, 38 insertions, 46 deletions
diff --git a/plugins/ltac/plugin_base.dune b/plugins/ltac/dune
index 5611f5ba16..6558ecbfe8 100644
--- a/plugins/ltac/plugin_base.dune
+++ b/plugins/ltac/dune
@@ -11,3 +11,5 @@
(synopsis "Coq's tauto tactic")
(modules tauto)
(libraries coq.plugins.ltac))
+
+(coq.pp (modules extratactics g_tactic g_rewrite g_eqdecide g_auto g_obligations g_ltac profile_ltac_tactics coretactics g_class extraargs))
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 7b1aa7a07a..7754fe401e 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -346,7 +346,7 @@ open Vars
let constr_flags () = {
Pretyping.use_typeclasses = Pretyping.UseTC;
- Pretyping.solve_unification_constraints = Pfedit.use_unification_heuristics ();
+ Pretyping.solve_unification_constraints = Proof.use_unification_heuristics ();
Pretyping.fail_evar = false;
Pretyping.expand_evars = true;
Pretyping.program_mode = false;
@@ -918,7 +918,7 @@ END
VERNAC COMMAND EXTEND GrabEvars STATE proof
| [ "Grab" "Existential" "Variables" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.V82.grab_evars p) pstate }
END
(* Shelves all the goals under focus. *)
@@ -950,7 +950,7 @@ END
VERNAC COMMAND EXTEND Unshelve STATE proof
| [ "Unshelve" ]
=> { classify_as_proofstep }
- -> { fun ~pstate -> Proof_global.map_proof (fun p -> Proof.unshelve p) pstate }
+ -> { fun ~pstate -> Declare.Proof.map_proof (fun p -> Proof.unshelve p) pstate }
END
(* Gives up on the goals under focus: the goals are considered solved,
@@ -1102,7 +1102,7 @@ END
VERNAC COMMAND EXTEND OptimizeProof
| ![ proof ] [ "Optimize" "Proof" ] => { classify_as_proofstep } ->
- { fun ~pstate -> Proof_global.compact_the_proof pstate }
+ { fun ~pstate -> Declare.Proof.compact pstate }
| [ "Optimize" "Heap" ] => { classify_as_proofstep } ->
{ Gc.compact () }
END
diff --git a/plugins/ltac/g_ltac.mlg b/plugins/ltac/g_ltac.mlg
index 50c3ed1248..e713ab13b2 100644
--- a/plugins/ltac/g_ltac.mlg
+++ b/plugins/ltac/g_ltac.mlg
@@ -359,23 +359,17 @@ open Vernacextend
open Goptions
open Libnames
-let print_info_trace = ref None
-
-let () = declare_int_option {
- optdepr = false;
- optkey = ["Info" ; "Level"];
- optread = (fun () -> !print_info_trace);
- optwrite = fun n -> print_info_trace := n;
-}
+let print_info_trace =
+ declare_intopt_option_and_ref ~depr:false ~key:["Info" ; "Level"]
let vernac_solve ~pstate n info tcom b =
let open Goal_select in
- let pstate, status = Proof_global.map_fold_proof_endline (fun etac p ->
+ let pstate, status = Declare.Proof.map_fold_proof_endline (fun etac p ->
let with_end_tac = if b then Some etac else None in
let global = match n with SelectAll | SelectList _ -> true | _ -> false in
- let info = Option.append info !print_info_trace in
+ let info = Option.append info (print_info_trace ()) in
let (p,status) =
- Pfedit.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
+ Proof.solve n info (Tacinterp.hide_interp global tcom None) ?with_end_tac p
in
(* in case a strict subtree was completed,
go back to the top of the prooftree *)
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 321b05b97c..35e131020b 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -639,7 +639,7 @@ let solve_remaining_by env sigma holes by =
let env = Environ.reset_with_named_context evi.evar_hyps env in
let ty = evi.evar_concl in
let name, poly = Id.of_string "rewrite", false in
- let c, sigma = Pfedit.refine_by_tactic ~name ~poly env sigma ty solve_tac in
+ let c, sigma = Proof.refine_by_tactic ~name ~poly env sigma ty solve_tac in
Evd.define evk (EConstr.of_constr c) sigma
in
List.fold_left solve sigma indep
@@ -1864,14 +1864,14 @@ let proper_projection env sigma r ty =
Array.append args [| instarg |]) in
it_mkLambda_or_LetIn app ctx
-let declare_projection n instance_id r =
+let declare_projection name instance_id r =
let poly = Global.is_polymorphic r in
let env = Global.env () in
let sigma = Evd.from_env env in
let sigma,c = Evd.fresh_global env sigma r in
let ty = Retyping.get_type_of env sigma c in
- let term = proper_projection env sigma c ty in
- let sigma, typ = Typing.type_of env sigma term in
+ let body = proper_projection env sigma c ty in
+ let sigma, typ = Typing.type_of env sigma body in
let ctx, typ = decompose_prod_assum sigma typ in
let typ =
let n =
@@ -1892,14 +1892,11 @@ let declare_projection n instance_id r =
let ctx,ccl = Reductionops.splay_prod_n env sigma (3 * n) typ
in it_mkProd_or_LetIn ccl ctx
in
- let typ = it_mkProd_or_LetIn typ ctx in
- let univs = Evd.univ_entry ~poly sigma in
- let typ = EConstr.to_constr sigma typ in
- let term = EConstr.to_constr sigma term in
- let cst = Declare.definition_entry ~types:typ ~univs term in
- let _ : Constant.t =
- Declare.declare_constant ~name:n ~kind:Decls.(IsDefinition Definition)
- (Declare.DefinitionEntry cst)
+ let types = Some (it_mkProd_or_LetIn typ ctx) in
+ let kind, opaque, scope = Decls.(IsDefinition Definition), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let impargs, udecl = [], UState.default_univ_decl in
+ let _r : GlobRef.t =
+ DeclareDef.declare_definition ~name ~scope ~kind ~opaque ~impargs ~udecl ~poly ~types ~body sigma
in ()
let build_morphism_signature env sigma m =
@@ -1927,10 +1924,7 @@ let build_morphism_signature env sigma m =
in
let morph = e_app_poly env evd (PropGlobal.proper_type env) [| t; sig_; m |] in
let evd = solve_constraints env !evd in
- let evd = Evd.minimize_universes evd in
- let m = Evarutil.nf_evars_universes evd (EConstr.Unsafe.to_constr morph) in
- Pretyping.check_evars env evd (EConstr.of_constr m);
- Evd.evar_universe_context evd, m
+ evd, morph
let default_morphism sign m =
let env = Global.env () in
@@ -1965,22 +1959,24 @@ let add_morphism_as_parameter atts m n : unit =
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
let evd = Evd.from_env env in
- let uctx, instance = build_morphism_signature env evd m in
- let uctx = UState.univ_entry ~poly:atts.polymorphic uctx in
- let cst = Declare.declare_constant ~name:instance_id
- ~kind:Decls.(IsAssumption Logical)
- (Declare.ParameterEntry (None,(instance,uctx),None))
- in
- Classes.add_instance (Classes.mk_instance
- (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global (GlobRef.ConstRef cst));
- declare_projection n instance_id (GlobRef.ConstRef cst)
+ let poly = atts.polymorphic in
+ let kind, opaque, scope = Decls.(IsAssumption Logical), false, DeclareDef.Global Declare.ImportDefaultBehavior in
+ let impargs, udecl = [], UState.default_univ_decl in
+ let evd, types = build_morphism_signature env evd m in
+ let evd, pe = DeclareDef.prepare_parameter ~poly ~udecl ~types evd in
+ let cst = Declare.declare_constant ~name:instance_id ~kind (Declare.ParameterEntry pe) in
+ let cst = GlobRef.ConstRef cst in
+ Classes.add_instance
+ (Classes.mk_instance
+ (PropGlobal.proper_class env evd) Hints.empty_hint_info atts.global cst);
+ declare_projection n instance_id cst
let add_morphism_interactive atts m n : Lemmas.t =
init_setoid ();
let instance_id = add_suffix n "_Proper" in
let env = Global.env () in
let evd = Evd.from_env env in
- let uctx, instance = build_morphism_signature env evd m in
+ let evd, morph = build_morphism_signature env evd m in
let poly = atts.polymorphic in
let kind = Decls.(IsDefinition Instance) in
let tac = make_tactic "Coq.Classes.SetoidTactics.add_morphism_tactic" in
@@ -1996,7 +1992,7 @@ let add_morphism_interactive atts m n : Lemmas.t =
let info = Lemmas.Info.make ~hook ~kind () in
Flags.silently
(fun () ->
- let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info (Evd.from_ctx uctx) (EConstr.of_constr instance) in
+ let lemma = Lemmas.start_lemma ~name:instance_id ~poly ~info evd morph in
fst (Lemmas.by (Tacinterp.interp tac) lemma)) ()
let add_morphism atts binders m s n =
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 4127d28bae..9910796d9c 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -299,7 +299,7 @@ let classify_tactic_notation tacobj = Substitute tacobj
let inTacticGrammar : tactic_grammar_obj -> obj =
declare_object {(default_object "TacticGrammar") with
- open_function = open_tactic_notation;
+ open_function = simple_open open_tactic_notation;
load_function = load_tactic_notation;
cache_function = cache_tactic_notation;
subst_function = subst_tactic_notation;
diff --git a/plugins/ltac/tacenv.ml b/plugins/ltac/tacenv.ml
index ce9189792e..76d47f5482 100644
--- a/plugins/ltac/tacenv.ml
+++ b/plugins/ltac/tacenv.ml
@@ -182,7 +182,7 @@ let inMD : bool * ltac_constant option * bool * glob_tactic_expr *
declare_object {(default_object "TAC-DEFINITION") with
cache_function = cache_md;
load_function = load_md;
- open_function = open_md;
+ open_function = simple_open open_md;
subst_function = subst_md;
classify_function = classify_md}
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index b0e26e1def..dda7f0742c 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2070,7 +2070,7 @@ let _ =
*)
let name, poly = Id.of_string "ltac_gen", poly in
let name, poly = Id.of_string "ltac_gen", poly in
- let (c, sigma) = Pfedit.refine_by_tactic ~name ~poly env sigma ty tac in
+ let (c, sigma) = Proof.refine_by_tactic ~name ~poly env sigma ty tac in
(EConstr.of_constr c, sigma)
in
GlobEnv.register_constr_interp0 wit_tactic eval
diff --git a/plugins/ltac/tactic_option.ml b/plugins/ltac/tactic_option.ml
index 4f00f17892..922d2f7792 100644
--- a/plugins/ltac/tactic_option.ml
+++ b/plugins/ltac/tactic_option.ml
@@ -32,7 +32,7 @@ let declare_tactic_option ?(default=Tacexpr.TacId []) name =
{ (default_object name) with
cache_function = cache;
load_function = (fun _ -> load);
- open_function = (fun _ -> load);
+ open_function = simple_open (fun _ -> load);
classify_function = (fun (local, tac) ->
if local then Dispose else Substitute (local, tac));
subst_function = subst}
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-08 03:27:31 +0000