aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/cc/ccalgo.ml2
-rw-r--r--plugins/derive/derive.ml2
-rw-r--r--plugins/extraction/mlutil.ml10
-rw-r--r--plugins/firstorder/sequent.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml18
-rw-r--r--plugins/funind/g_indfun.ml46
-rw-r--r--plugins/funind/indfun_common.ml24
-rw-r--r--plugins/funind/invfun.ml6
-rw-r--r--plugins/funind/recdef.ml16
-rw-r--r--plugins/ltac/coretactics.ml46
-rw-r--r--plugins/ltac/evar_tactics.ml2
-rw-r--r--plugins/ltac/extratactics.ml418
-rw-r--r--plugins/ltac/g_auto.ml42
-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.ml7
-rw-r--r--plugins/ltac/rewrite.ml2
-rw-r--r--plugins/omega/coq_omega.ml7
-rw-r--r--plugins/setoid_ring/newring.ml50
-rw-r--r--plugins/ssr/ssrequality.ml5
-rw-r--r--plugins/ssr/ssrvernac.ml47
-rw-r--r--plugins/ssr/ssrview.ml2
-rw-r--r--plugins/ssrmatching/ssrmatching.ml46
24 files changed, 114 insertions, 100 deletions
diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 8e53a044d7..4c6156a38b 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -457,7 +457,7 @@ let rec canonize_name sigma c =
| LetIn (na,b,t,ct) ->
mkLetIn (na, func b,func t,func ct)
| App (ct,l) ->
- mkApp (func ct,Array.smartmap func l)
+ mkApp (func ct,Array.Smart.map func l)
| Proj(p,c) ->
let p' = Projection.map (fun kn ->
Constant.make1 (Constant.canonical kn)) p in
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 8a55538bde..480819ebe1 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -61,7 +61,7 @@ let start_deriving f suchthat lemma =
| Proved (opaque, None, obj) ->
match Proof_global.(obj.entries) with
| [_;f_def;lemma_def] ->
- opaque <> Vernacexpr.Transparent , f_def , lemma_def
+ opaque <> Proof_global.Transparent , f_def , lemma_def
| _ -> assert false
in
(** The opacity of [f_def] is adjusted to be [false], as it
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 0901acc7d9..9f5c1f1a17 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -541,24 +541,24 @@ let dump_unused_vars a =
| MLcase (t,e,br) ->
let e' = ren env e in
- let br' = Array.smartmap (ren_branch env) br in
+ let br' = Array.Smart.map (ren_branch env) br in
if e' == e && br' == br then a else MLcase (t,e',br')
| MLfix (i,ids,v) ->
let env' = List.init (Array.length ids) (fun _ -> ref false) @ env in
- let v' = Array.smartmap (ren env') v in
+ let v' = Array.Smart.map (ren env') v in
if v' == v then a else MLfix (i,ids,v')
| MLapp (b,l) ->
- let b' = ren env b and l' = List.smartmap (ren env) l in
+ let b' = ren env b and l' = List.Smart.map (ren env) l in
if b' == b && l' == l then a else MLapp (b',l')
| MLcons(t,r,l) ->
- let l' = List.smartmap (ren env) l in
+ let l' = List.Smart.map (ren env) l in
if l' == l then a else MLcons (t,r,l')
| MLtuple l ->
- let l' = List.smartmap (ren env) l in
+ let l' = List.Smart.map (ren env) l in
if l' == l then a else MLtuple l'
| MLmagic b ->
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 0c752d4a48..2a527da9be 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -229,7 +229,9 @@ let extend_with_auto_hints env sigma l seq =
let print_cmap map=
let print_entry c l s=
- let xc=Constrextern.extern_constr false (Global.env ()) Evd.empty (EConstr.of_constr c) in
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ let xc=Constrextern.extern_constr false env sigma (EConstr.of_constr c) in
str "| " ++
prlist Printer.pr_global l ++
str " : " ++
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 3801fec4b3..5336948642 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -230,7 +230,7 @@ let isAppConstruct ?(env=Global.env ()) sigma t =
with Not_found -> false
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env @@ Evd.from_env Environ.empty_env
exception NoChange
@@ -598,7 +598,7 @@ let treat_new_case ptes_infos nb_prod continue_tac term dyn_infos =
Proofview.V82.of_tactic (intro_using heq_id);
onLastHypId (fun heq_id -> tclTHENLIST [
(* Then the new hypothesis *)
- tclMAP (fun id -> Proofview.V82.of_tactic (introduction ~check:false id)) dyn_infos.rec_hyps;
+ tclMAP (fun id -> Proofview.V82.of_tactic (introduction id)) dyn_infos.rec_hyps;
observe_tac "after_introduction" (fun g' ->
(* We get infos on the equations introduced*)
let new_term_value_eq = pf_unsafe_type_of g' (mkVar heq_id) in
@@ -1013,7 +1013,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
lemma_type
(Lemmas.mk_hook (fun _ _ -> ()));
ignore (Pfedit.by (Proofview.V82.tactic prove_replacement));
- Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None)));
+ Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None)));
evd
@@ -1099,10 +1099,12 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
let get_body const =
match Global.body_of_constant const with
| Some (body, _) ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- (Global.env ())
- (Evd.empty)
+ env
+ sigma
(EConstr.of_constr body)
| None -> user_err Pp.(str "Cannot define a principle over an axiom ")
in
@@ -1242,7 +1244,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
if this_fix_info.idx + 1 = 0
then tclIDTAC (* Someone tries to defined a principle on a fully parametric definition declared as a fixpoint (strange but ....) *)
else
- observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix (Some this_fix_info.name) (this_fix_info.idx +1)))
+ observe_tac_stream (str "h_fix " ++ int (this_fix_info.idx +1) ) (Proofview.V82.of_tactic (fix this_fix_info.name (this_fix_info.idx +1)))
else
Proofview.V82.of_tactic (Tactics.mutual_fix this_fix_info.name (this_fix_info.idx + 1)
other_fix_infos 0)
@@ -1340,7 +1342,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
nb_rec_hyps = -100;
rec_hyps = [];
info =
- Reductionops.nf_betaiota (pf_env g) Evd.empty
+ Reductionops.nf_betaiota (pf_env g) (project g)
(applist(fbody_with_full_params,
(List.rev_map var_of_decl princ_params)@
(List.rev_map mkVar args_id)
@@ -1657,7 +1659,7 @@ let prove_principle_for_gen
(* observe_tac "reverting" *) (revert (List.rev (acc_rec_arg_id::args_ids)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl () ++ *)
(* str "fix arg num" ++ int (List.length args_ids + 1) ); tclIDTAC g); *)
- (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
+ (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix fix_id (List.length args_ids + 1)));
(* (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
h_intros (List.rev (acc_rec_arg_id::args_ids));
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 90af20b4ca..0a2741ad15 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -38,7 +38,9 @@ let pr_fun_ind_using_typed prc prlc _ opt_c =
match opt_c with
| None -> mt ()
| Some b ->
- let (_, b) = b (Global.env ()) Evd.empty in
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let (_, b) = b env evd in
spc () ++ hov 2 (str "using" ++ spc () ++ Miscprint.pr_with_bindings prc prlc b)
@@ -123,7 +125,7 @@ ARGUMENT EXTEND auto_using'
END
module Gram = Pcoq.Gram
-module Vernac = Pcoq.Vernac_
+module Vernac = Pvernac.Vernac_
module Tactic = Pltac
type function_rec_definition_loc_argtype = (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) Loc.located
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 35c3acd411..b0c9ff8fcb 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -269,12 +269,12 @@ let subst_Function (subst,finfos) =
in
let function_constant' = do_subst_con finfos.function_constant in
let graph_ind' = do_subst_ind finfos.graph_ind in
- let equation_lemma' = Option.smartmap do_subst_con finfos.equation_lemma in
- let correctness_lemma' = Option.smartmap do_subst_con finfos.correctness_lemma in
- let completeness_lemma' = Option.smartmap do_subst_con finfos.completeness_lemma in
- let rect_lemma' = Option.smartmap do_subst_con finfos.rect_lemma in
- let rec_lemma' = Option.smartmap do_subst_con finfos.rec_lemma in
- let prop_lemma' = Option.smartmap do_subst_con finfos.prop_lemma in
+ let equation_lemma' = Option.Smart.map do_subst_con finfos.equation_lemma in
+ let correctness_lemma' = Option.Smart.map do_subst_con finfos.correctness_lemma in
+ let completeness_lemma' = Option.Smart.map do_subst_con finfos.completeness_lemma in
+ let rect_lemma' = Option.Smart.map do_subst_con finfos.rect_lemma in
+ let rec_lemma' = Option.Smart.map do_subst_con finfos.rec_lemma in
+ let prop_lemma' = Option.Smart.map do_subst_con finfos.prop_lemma in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
equation_lemma' == finfos.equation_lemma &&
@@ -302,12 +302,12 @@ let classify_Function infos = Libobject.Substitute infos
let discharge_Function (_,finfos) =
let function_constant' = Lib.discharge_con finfos.function_constant
and graph_ind' = Lib.discharge_inductive finfos.graph_ind
- and equation_lemma' = Option.smartmap Lib.discharge_con finfos.equation_lemma
- and correctness_lemma' = Option.smartmap Lib.discharge_con finfos.correctness_lemma
- and completeness_lemma' = Option.smartmap Lib.discharge_con finfos.completeness_lemma
- and rect_lemma' = Option.smartmap Lib.discharge_con finfos.rect_lemma
- and rec_lemma' = Option.smartmap Lib.discharge_con finfos.rec_lemma
- and prop_lemma' = Option.smartmap Lib.discharge_con finfos.prop_lemma
+ and equation_lemma' = Option.Smart.map Lib.discharge_con finfos.equation_lemma
+ and correctness_lemma' = Option.Smart.map Lib.discharge_con finfos.correctness_lemma
+ and completeness_lemma' = Option.Smart.map Lib.discharge_con finfos.completeness_lemma
+ and rect_lemma' = Option.Smart.map Lib.discharge_con finfos.rect_lemma
+ and rec_lemma' = Option.Smart.map Lib.discharge_con finfos.rec_lemma
+ and prop_lemma' = Option.Smart.map Lib.discharge_con finfos.prop_lemma
in
if function_constant' == finfos.function_constant &&
graph_ind' == finfos.graph_ind &&
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 1809526356..cc92a73f02 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -67,7 +67,7 @@ let observe_tac s tac g =
let nf_zeta =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
Environ.empty_env
- Evd.empty
+ (Evd.from_env Environ.empty_env)
let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
@@ -818,7 +818,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
(proving_tac i))));
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
(* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
let _,lem_cst_constr = Evd.fresh_global
@@ -879,7 +879,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive list
ignore (Pfedit.by
(Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
(proving_tac i)))) ;
- (Lemmas.save_proof (Vernacexpr.(Proved(Transparent,None))));
+ (Lemmas.save_proof (Vernacexpr.(Proved(Proof_global.Transparent,None))));
let finfo = find_Function_infos (fst f_as_constant) in
let _,lem_cst_constr = Evd.fresh_global
(Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 2464c595f5..72bb8253d1 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -72,7 +72,7 @@ let declare_fun f_id kind ?univs value =
let ce = definition_entry ?univs value (*FIXME *) in
ConstRef(declare_constant f_id (DefinitionEntry ce, kind));;
-let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Transparent,None)))
+let defined () = Lemmas.save_proof (Vernacexpr.(Proved (Proof_global.Transparent,None)))
let def_of_const t =
match (Constr.kind t) with
@@ -106,12 +106,12 @@ let const_of_ref = function
let nf_zeta env =
Reductionops.clos_norm_flags (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
- env
- Evd.empty
+ env (Evd.from_env env)
let nf_betaiotazeta = (* Reductionops.local_strong Reductionops.whd_betaiotazeta *)
- Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env Evd.empty
+ Reductionops.clos_norm_flags CClosure.betaiotazeta Environ.empty_env
+ (Evd.from_env Environ.empty_env)
@@ -1152,7 +1152,7 @@ let termination_proof_header is_mes input_type ids args_id relation
tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (Proofview.V82.of_tactic (clear [id])))
))
;
- observe_tac (str "fix") (Proofview.V82.of_tactic (fix (Some hrec) (nargs+1)));
+ observe_tac (str "fix") (Proofview.V82.of_tactic (fix hrec (nargs+1)));
h_intros args_id;
Proofview.V82.of_tactic (Simple.intro wf_rec_arg);
observe_tac (str "tac") (tac wf_rec_arg hrec wf_rec_arg acc_inv)
@@ -1306,9 +1306,9 @@ let build_new_goal_type () =
let is_opaque_constant c =
let cb = Global.lookup_constant c in
match cb.Declarations.const_body with
- | Declarations.OpaqueDef _ -> Vernacexpr.Opaque
- | Declarations.Undef _ -> Vernacexpr.Opaque
- | Declarations.Def _ -> Vernacexpr.Transparent
+ | Declarations.OpaqueDef _ -> Proof_global.Opaque
+ | Declarations.Undef _ -> Proof_global.Opaque
+ | Declarations.Def _ -> Proof_global.Transparent
let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decompose_and_tac,nb_goal) =
(* Pp.msgnl (str "gls_type := " ++ Printer.pr_lconstr gls_type); *)
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..5463893ad0 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -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/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 797dfbe23f..17011f2067 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -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..07047d0162 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -219,7 +219,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..3dfe308a5d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -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/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/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index e455ebb285..3594c87653 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -369,8 +369,11 @@ let coq_True = lazy (init_constant "True")
(* uses build_coq_and, build_coq_not, build_coq_or, build_coq_ex *)
(* For unfold *)
-let evaluable_ref_of_constr s c = match EConstr.kind Evd.empty (Lazy.force c) with
- | Const (kn,u) when Tacred.is_evaluable (Global.env()) (EvalConstRef kn) ->
+let evaluable_ref_of_constr s c =
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ match EConstr.kind evd (Lazy.force c) with
+ | Const (kn,u) when Tacred.is_evaluable env (EvalConstRef kn) ->
EvalConstRef kn
| _ -> anomaly ~label:"Coq_omega" (Pp.str (s^" is not an evaluable constant."))
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 59ba4b7de4..b9d0d2e251 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -40,11 +40,7 @@ let error msg = CErrors.user_err Pp.(str msg)
type protect_flag = Eval|Prot|Rec
-let tag_arg tag_rec map subs i c =
- match map i with
- Eval -> mk_clos subs c
- | Prot -> mk_atom c
- | Rec -> if Int.equal i (-1) then mk_clos subs c else tag_rec c
+type protection = Evd.evar_map -> EConstr.t -> GlobRef.t -> (Int.t -> protect_flag) option
let global_head_of_constr sigma c =
let f, args = decompose_app sigma c in
@@ -55,32 +51,24 @@ let global_of_constr_nofail c =
try global_of_constr c
with Not_found -> VarRef (Id.of_string "dummy")
-let rec mk_clos_but f_map subs t =
- let open Term in
- match f_map (global_of_constr_nofail t) with
- | Some map -> tag_arg (mk_clos_but f_map subs) map subs (-1) t
- | None ->
- (match Constr.kind t with
- App(f,args) -> mk_clos_app_but f_map subs f args 0
- | Prod _ -> mk_clos_deep (mk_clos_but f_map) subs t
- | _ -> mk_atom t)
+let rec mk_clos_but f_map n t =
+ let (f, args) = Constr.decompose_appvect t in
+ match f_map (global_of_constr_nofail f) with
+ | Some tag ->
+ let map i t = tag_arg f_map n (tag i) t in
+ if Array.is_empty args then map (-1) f
+ else mk_red (FApp (map (-1) f, Array.mapi map args))
+ | None -> mk_atom t
-and mk_clos_app_but f_map subs f args n =
- let open Constr in
- if n >= Array.length args then mk_atom(mkApp(f, args))
- else
- let fargs, args' = Array.chop n args in
- let f' = mkApp(f,fargs) in
- match f_map (global_of_constr_nofail f') with
- | Some map ->
- let f i t = tag_arg (mk_clos_but f_map subs) map subs i t in
- mk_red (FApp (f (-1) f', Array.mapi f args'))
- | None -> mk_atom (mkApp (f, args))
+and tag_arg f_map n tag c = match tag with
+| Eval -> mk_clos (Esubst.subs_id n) c
+| Prot -> mk_atom c
+| Rec -> mk_clos_but f_map n c
let interp_map l t =
try Some(List.assoc_f GlobRef.equal t l) with Not_found -> None
-let protect_maps = ref String.Map.empty
+let protect_maps : protection String.Map.t ref = ref String.Map.empty
let add_map s m = protect_maps := String.Map.add s m !protect_maps
let lookup_map map =
try String.Map.find map !protect_maps
@@ -90,8 +78,14 @@ let lookup_map map =
let protect_red map env sigma c0 =
let evars ev = Evarutil.safe_evar_value sigma ev in
let c = EConstr.Unsafe.to_constr c0 in
- EConstr.of_constr (kl (create_clos_infos ~evars all env) (create_tab ())
- (mk_clos_but (lookup_map map sigma c0) (Esubst.subs_id 0) c));;
+ let tab = create_tab () in
+ let infos = create_clos_infos ~evars all env in
+ let map = lookup_map map sigma c0 in
+ let rec eval n c = match Constr.kind c with
+ | Prod (na, t, u) -> Constr.mkProd (na, eval n t, eval (n + 1) u)
+ | _ -> kl infos tab (mk_clos_but map n c)
+ in
+ EConstr.of_constr (eval 0 c)
let protect_tac map =
Tactics.reduct_option (protect_red map,DEFAULTcast) None
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index a310229199..f929e94309 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -287,7 +287,10 @@ let foldtac occ rdx ft gl =
(fun env c _ h -> try find_T env c h ~k:(fun env t _ _ -> t) with NoMatch ->c),
(fun () -> try end_T () with NoMatch -> fake_pmatcher_end ())
| _ ->
- (fun env c _ h -> try let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in EConstr.to_constr sigma (EConstr.of_constr t)
+ (fun env c _ h ->
+ try
+ let sigma = unify_HO env sigma (EConstr.of_constr c) (EConstr.of_constr t) in
+ EConstr.to_constr ~abort_on_undefined_evars:false sigma (EConstr.of_constr t)
with _ -> errorstrm Pp.(str "fold pattern " ++ pr_constr_pat t ++ spc ()
++ str "does not match redex " ++ pr_constr_pat c)),
fake_pmatcher_end in
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 05dbf0a86d..750461a1bf 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -19,7 +19,7 @@ open Constrexpr_ops
open Pcoq
open Pcoq.Prim
open Pcoq.Constr
-open Pcoq.Vernac_
+open Pvernac.Vernac_
open Ltac_plugin
open Notation_ops
open Notation_term
@@ -377,7 +377,10 @@ let interp_head_pat hpat =
| Cast (c', _, _) -> loop c'
| Prod (_, _, c') -> loop c'
| LetIn (_, _, _, c') -> loop c'
- | _ -> Constr_matching.is_matching (Global.env()) Evd.empty p (EConstr.of_constr c) in
+ | _ ->
+ let env = Global.env () in
+ let sigma = Evd.from_env env in
+ Constr_matching.is_matching env sigma p (EConstr.of_constr c) in
filter_head, loop
let all_true _ = true
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index fc50b24a60..29a936381f 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -260,7 +260,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
let p = Reductionops.nf_evar sigma p in
let get_body = function Evd.Evar_defined x -> x | _ -> assert false in
let evars_of_econstr sigma t =
- Evd.evars_of_term (EConstr.to_constr sigma (EConstr.of_constr t)) in
+ Evarutil.undefined_evars_of_term sigma (EConstr.of_constr t) in
let rigid_of s =
List.fold_left (fun l k ->
if Evd.is_defined sigma k then
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0dd3625ba2..93c63d522a 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -708,9 +708,9 @@ let match_upats_HO ~on_instance upats env sigma0 ise c =
;;
-let fixed_upat = function
+let fixed_upat evd = function
| {up_k = KpatFlex | KpatEvar _ | KpatProj _} -> false
-| {up_t = t} -> not (occur_existential Evd.empty (EConstr.of_constr t)) (** FIXME *)
+| {up_t = t} -> not (occur_existential evd (EConstr.of_constr t)) (** FIXME *)
let do_once r f = match !r with Some _ -> () | None -> r := Some (f ())
@@ -769,7 +769,7 @@ let mk_tpattern_matcher ?(all_instances=false)
let p2t p = mkApp(p.up_f,p.up_a) in
let source () = match upats_origin, upats with
| None, [p] ->
- (if fixed_upat p then str"term " else str"partial term ") ++
+ (if fixed_upat ise p then str"term " else str"partial term ") ++
pr_constr_pat (p2t p) ++ spc()
| Some (dir,rule), [p] -> str"The " ++ pr_dir_side dir ++ str" of " ++
pr_constr_pat rule ++ fnl() ++ ws 4 ++ pr_constr_pat (p2t p) ++ fnl()
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 10:53:05 +0000