aboutsummaryrefslogtreecommitdiff
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml46
-rw-r--r--plugins/ltac/evar_tactics.ml4
-rw-r--r--plugins/ltac/extraargs.ml42
-rw-r--r--plugins/ltac/extraargs.mli2
-rw-r--r--plugins/ltac/extratactics.ml420
-rw-r--r--plugins/ltac/g_auto.ml45
-rw-r--r--plugins/ltac/g_ltac.ml48
-rw-r--r--plugins/ltac/g_rewrite.ml42
-rw-r--r--plugins/ltac/g_tactic.ml42
-rw-r--r--plugins/ltac/pptactic.ml9
-rw-r--r--plugins/ltac/pptactic.mli4
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/ltac/tacsubst.ml2
-rw-r--r--plugins/ltac/tauto.ml2
14 files changed, 38 insertions, 32 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 931633e1a8..faa9e413bb 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -273,15 +273,13 @@ END
(* Fix *)
TACTIC EXTEND fix
- [ "fix" natural(n) ] -> [ Tactics.fix None n ]
-| [ "fix" ident(id) natural(n) ] -> [ Tactics.fix (Some id) n ]
+ [ "fix" ident(id) natural(n) ] -> [ Tactics.fix id n ]
END
(* Cofix *)
TACTIC EXTEND cofix
- [ "cofix" ] -> [ Tactics.cofix None ]
-| [ "cofix" ident(id) ] -> [ Tactics.cofix (Some id) ]
+ [ "cofix" ident(id) ] -> [ Tactics.cofix id ]
END
(* Clear *)
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index fb6be430fc..ea8dcf57dd 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -10,7 +10,7 @@
open Util
open Names
-open Term
+open Constr
open CErrors
open Evar_refiner
open Tacmach
@@ -52,7 +52,7 @@ let instantiate_tac n c ido =
match ido with
ConclLocation () -> evar_list sigma (pf_concl gl)
| HypLocation (id,hloc) ->
- let decl = Environ.lookup_named_val id (Goal.V82.hyps sigma (sig_it gl)) in
+ let decl = Environ.lookup_named id (pf_env gl) in
match hloc with
InHyp ->
(match decl with
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index 702b830342..4e7c8b754f 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -251,7 +251,7 @@ END
let pr_by_arg_tac _prc _prlc prtac opt_c =
match opt_c with
| None -> mt ()
- | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_term.E) t)
+ | Some t -> hov 2 (str "by" ++ spc () ++ prtac (3,Notation_gram.E) t)
ARGUMENT EXTEND by_arg_tac
TYPED AS tactic_opt
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index e5a4f090ed..ff697e3c75 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -66,7 +66,7 @@ val wit_by_arg_tac :
Geninterp.Val.t option) Genarg.genarg_type
val pr_by_arg_tac :
- (int * Notation_term.parenRelation -> raw_tactic_expr -> Pp.t) ->
+ (int * Notation_gram.parenRelation -> raw_tactic_expr -> Pp.t) ->
raw_tactic_expr option -> Pp.t
val test_lpar_id_colon : unit Pcoq.Gram.entry
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23f..c5254b37c9 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -9,6 +9,7 @@
(************************************************************************)
open Pp
+open Constr
open Genarg
open Stdarg
open Tacarg
@@ -286,7 +287,6 @@ END
(**********************************************************************)
(* Hint Resolve *)
-open Term
open EConstr
open Vars
open Coqlib
@@ -320,7 +320,7 @@ let project_hint ~poly pri l2r r =
let add_hints_iff ~atts l2r lc n bl =
let open Vernacinterp in
- Hints.add_hints (Locality.make_module_locality atts.locality) bl
+ Hints.add_hints ~local:(Locality.make_module_locality atts.locality) bl
(Hints.HintsResolveEntry (List.map (project_hint ~poly:atts.polymorphic n l2r) lc))
VERNAC COMMAND FUNCTIONAL EXTEND HintResolveIffLR CLASSIFIED AS SIDEFF
@@ -613,10 +613,12 @@ END
VERNAC COMMAND EXTEND RetroknowledgeRegister CLASSIFIED AS SIDEFF
| [ "Register" constr(c) "as" retroknowledge_field(f) "by" constr(b)] ->
- [ let tc,_ctx = Constrintern.interp_constr (Global.env ()) Evd.empty c in
- let tb,_ctx(*FIXME*) = Constrintern.interp_constr (Global.env ()) Evd.empty b in
- let tc = EConstr.to_constr Evd.empty tc in
- let tb = EConstr.to_constr Evd.empty tb in
+ [ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let tc,_ctx = Constrintern.interp_constr env evd c in
+ let tb,_ctx(*FIXME*) = Constrintern.interp_constr env evd b in
+ let tc = EConstr.to_constr evd tc in
+ let tb = EConstr.to_constr evd tb in
Global.register f tc tb ]
END
@@ -779,7 +781,7 @@ let mkCaseEq a : unit Proofview.tactic =
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
(** FIXME: this looks really wrong. Does anybody really use this tactic? *)
- let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env Evd.empty concl in
+ let (_, c) = Tacred.pattern_occs [Locus.OnlyOccurrences [1], a] env (Evd.from_env env) concl in
change_concl c
end;
simplest_case a]
@@ -1106,7 +1108,9 @@ END
VERNAC COMMAND EXTEND Declare_keys CLASSIFIED AS SIDEFF
| [ "Declare" "Equivalent" "Keys" constr(c) constr(c') ] -> [
let get_key c =
- let (evd, c) = Constrintern.interp_open_constr (Global.env ()) Evd.empty c in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let (evd, c) = Constrintern.interp_open_constr env evd c in
let kind c = EConstr.kind evd c in
Keys.constr_key kind c
in
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 643f7e99f7..642e521556 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -9,6 +9,7 @@
(************************************************************************)
open Pp
+open Constr
open Genarg
open Stdarg
open Pcoq.Prim
@@ -169,7 +170,7 @@ END
TACTIC EXTEND convert_concl_no_check
-| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x Term.DEFAULTcast ]
+| ["convert_concl_no_check" constr(x) ] -> [ Tactics.convert_concl_no_check x DEFAULTcast ]
END
let pr_pre_hints_path_atom _ _ _ = Hints.pp_hints_path_atom Libnames.pr_reference
@@ -219,7 +220,7 @@ VERNAC COMMAND FUNCTIONAL EXTEND HintCut CLASSIFIED AS SIDEFF
fun ~atts ~st -> begin
let open Vernacinterp in
let entry = Hints.HintsCutEntry (Hints.glob_hints_path p) in
- Hints.add_hints (Locality.make_section_locality atts.locality)
+ Hints.add_hints ~local:(Locality.make_section_locality atts.locality)
(match dbnames with None -> ["core"] | Some l -> l) entry;
st
end
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 4857beffa8..ed54320a59 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -21,9 +21,9 @@ open Tok (* necessary for camlp5 *)
open Names
open Pcoq
-open Pcoq.Constr
-open Pcoq.Vernac_
open Pcoq.Prim
+open Pcoq.Constr
+open Pvernac.Vernac_
open Pltac
let fail_default_value = ArgArg 0
@@ -58,8 +58,8 @@ let tacdef_body = new_entry "tactic:tacdef_body"
let _ =
let mode = {
Proof_global.name = "Classic";
- set = (fun () -> set_command_entry tactic_mode);
- reset = (fun () -> set_command_entry Pcoq.Vernac_.noedit_mode);
+ set = (fun () -> Pvernac.set_command_entry tactic_mode);
+ reset = (fun () -> Pvernac.(set_command_entry noedit_mode));
} in
Proof_global.register_proof_mode mode
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index fbaa2e58f7..079001ee40 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -20,9 +20,9 @@ open Extraargs
open Tacmach
open Rewrite
open Stdarg
-open Pcoq.Vernac_
open Pcoq.Prim
open Pcoq.Constr
+open Pvernac.Vernac_
open Pltac
DECLARE PLUGIN "ltac_plugin"
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 7534e27999..dc9f607cf0 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -211,7 +211,7 @@ let warn_deprecated_eqn_syntax =
(* Auxiliary grammar rules *)
-open Vernac_
+open Pvernac.Vernac_
GEXTEND Gram
GLOBAL: simple_tactic constr_with_bindings quantified_hypothesis
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bd02d85d59..b29af6680d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -18,7 +18,7 @@ open Genarg
open Geninterp
open Stdarg
open Libnames
-open Notation_term
+open Notation_gram
open Misctypes
open Locus
open Decl_kinds
@@ -149,9 +149,12 @@ let string_of_genarg_arg (ArgumentType arg) =
let open Genprint in
match generic_top_print (in_gen (Topwit wit) x) with
| TopPrinterBasic pr -> pr ()
- | TopPrinterNeedsContext pr -> pr (Global.env()) Evd.empty
+ | TopPrinterNeedsContext pr ->
+ let env = Global.env() in
+ pr env (Evd.from_env env)
| TopPrinterNeedsContextAndLevel { default_ensure_surrounded; printer } ->
- printer (Global.env()) Evd.empty default_ensure_surrounded
+ let env = Global.env() in
+ printer env (Evd.from_env env) default_ensure_surrounded
end
| _ -> default
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 799a52cc8b..5d2a996183 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -17,7 +17,7 @@ open Names
open Misctypes
open Environ
open Constrexpr
-open Notation_term
+open Notation_gram
open Tacexpr
type 'a grammar_tactic_prod_item_expr =
@@ -153,5 +153,5 @@ val pr_value : tolerability -> Val.t -> Pp.t
val ltop : tolerability
-val make_constr_printer : (env -> Evd.evar_map -> Notation_term.tolerability -> 'a -> Pp.t) ->
+val make_constr_printer : (env -> Evd.evar_map -> tolerability -> 'a -> Pp.t) ->
'a Genprint.top_printer
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 1b86583da1..b91315aca7 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1922,7 +1922,7 @@ let build_morphism_signature env sigma m =
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.empty evd (EConstr.of_constr m);
+ Pretyping.check_evars env (Evd.from_env env) evd (EConstr.of_constr m);
Evd.evar_universe_context evd, m
let default_morphism sign m =
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index a1d8b087e8..50bf687b1d 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -112,7 +112,7 @@ let subst_glob_constr_or_pattern subst (bvars,c,p) =
(bvars,subst_glob_constr subst c,subst_pattern subst p)
let subst_redexp subst =
- Miscops.map_red_expr_gen
+ Redops.map_red_expr_gen
(subst_glob_constr subst)
(subst_evaluable subst)
(subst_glob_constr_or_pattern subst)
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index a51c09ca4f..8eeb8903e7 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -8,7 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Term
+open Constr
open EConstr
open Hipattern
open Names
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 21:39:59 +0000