aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/derive/derive.ml5
-rw-r--r--plugins/funind/recdef.ml30
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/ssr/ssrequality.ml4
-rw-r--r--plugins/ssr/ssrview.ml4
-rw-r--r--plugins/ssrmatching/ssrmatching.ml8
6 files changed, 27 insertions, 26 deletions
diff --git a/plugins/derive/derive.ml b/plugins/derive/derive.ml
index 4425e41652..4769c2dc53 100644
--- a/plugins/derive/derive.ml
+++ b/plugins/derive/derive.ml
@@ -102,6 +102,7 @@ let start_deriving f suchthat lemma =
let terminator = Proof_global.make_terminator terminator in
let pstate = Proof_global.start_dependent_proof ~ontop:None lemma kind goals terminator in
- fst @@ Proof_global.with_current_proof begin fun _ p ->
- Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p
+ Proof_global.simple_with_current_proof begin fun _ p ->
+ let p,_,() = Proof.run_tactic env Proofview.(tclFOCUS 1 2 shelve) p in
+ p
end pstate
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 3dd3a430e8..1fca132655 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -132,7 +132,7 @@ let nat = function () -> (coq_init_constant "nat")
let iter_ref () =
try find_reference ["Recdef"] "iter"
with Not_found -> user_err Pp.(str "module Recdef not loaded")
-let iter_rd = function () -> (constr_of_global (delayed_force iter_ref))
+let iter_rd = function () -> (constr_of_monomorphic_global (delayed_force iter_ref))
let eq = function () -> (coq_init_constant "eq")
let le_lt_SS = function () -> (constant ["Recdef"] "le_lt_SS")
let le_lt_n_Sm = function () -> (coq_constant arith_Lt "le_lt_n_Sm")
@@ -145,7 +145,7 @@ let coq_O = function () -> (coq_init_constant "O")
let coq_S = function () -> (coq_init_constant "S")
let lt_n_O = function () -> (coq_constant arith_Nat "nlt_0_r")
let max_ref = function () -> (find_reference ["Recdef"] "max")
-let max_constr = function () -> EConstr.of_constr (constr_of_global (delayed_force max_ref))
+let max_constr = function () -> EConstr.of_constr (constr_of_monomorphic_global (delayed_force max_ref))
let f_S t = mkApp(delayed_force coq_S, [|t|]);;
@@ -1041,13 +1041,13 @@ let compute_terminate_type nb_args func =
let open Term in
let open Constr in
let open CVars in
- let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_global func)) in
+ let _,a_arrow_b,_ = destLambda(def_of_const (constr_of_monomorphic_global func)) in
let rev_args,b = decompose_prod_n nb_args a_arrow_b in
let left =
mkApp(delayed_force iter_rd,
Array.of_list
(lift 5 a_arrow_b:: mkRel 3::
- constr_of_global func::mkRel 1::
+ constr_of_monomorphic_global func::mkRel 1::
List.rev (List.map_i (fun i _ -> mkRel (6+i)) 0 rev_args)
)
)
@@ -1065,7 +1065,7 @@ let compute_terminate_type nb_args func =
delayed_force nat,
(mkProd (make_annot (Name k_id) Sorts.Relevant, delayed_force nat,
mkArrow cond Sorts.Relevant result))))|])in
- let value = mkApp(constr_of_global (Util.delayed_force coq_sig_ref),
+ let value = mkApp(constr_of_monomorphic_global (Util.delayed_force coq_sig_ref),
[|b;
(mkLambda (make_annot (Name v_id) Sorts.Relevant, b, nb_iter))|]) in
compose_prod rev_args value
@@ -1161,7 +1161,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
fun g ->
let sigma = project g in
let ids = Termops.ids_of_named_context (pf_hyps g) in
- let func_body = (def_of_const (constr_of_global func)) in
+ let func_body = (def_of_const (constr_of_monomorphic_global func)) in
let func_body = EConstr.of_constr func_body in
let (f_name, _, body1) = destLambda sigma func_body in
let f_id =
@@ -1222,7 +1222,7 @@ let whole_start (concl_tac:tactic) nb_args is_mes func input_type relation rec_a
let get_current_subgoals_types pstate =
let p = Proof_global.give_me_the_proof pstate in
- let sgs,_,_,_,sigma = Proof.proof p in
+ let Proof.{ goals=sgs; sigma; _ } = Proof.data p in
sigma, List.map (Goal.V82.abstract_type sigma) sgs
exception EmptySubgoals
@@ -1253,7 +1253,7 @@ let build_and_l sigma l =
let c,tac,nb = f pl in
mk_and p1 c,
tclTHENS
- (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_global conj_constr))))
+ (Proofview.V82.of_tactic (apply (EConstr.of_constr (constr_of_monomorphic_global conj_constr))))
[tclIDTAC;
tac
],nb+1
@@ -1437,7 +1437,7 @@ let start_equation (f:GlobRef.t) (term_f:GlobRef.t)
(cont_tactic:Id.t list -> tactic) g =
let sigma = project g in
let ids = pf_ids_of_hyps g in
- let terminate_constr = constr_of_global term_f in
+ let terminate_constr = constr_of_monomorphic_global term_f in
let terminate_constr = EConstr.of_constr terminate_constr in
let nargs = nb_prod (project g) (EConstr.of_constr (type_of_const sigma terminate_constr)) in
let x = n_x_id ids nargs in
@@ -1457,7 +1457,7 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
| _ -> anomaly ~label:"terminate_lemma" (Pp.str "not a constant.")
in
let evd = Evd.from_ctx uctx in
- let f_constr = constr_of_global f_ref in
+ let f_constr = constr_of_monomorphic_global f_ref in
let equation_lemma_type = subst1 f_constr equation_lemma_type in
let pstate = Lemmas.start_proof ~ontop:None eq_name (Global, false, Proof Lemma) ~sign evd
(EConstr.of_constr equation_lemma_type) in
@@ -1466,12 +1466,12 @@ let com_eqn sign uctx nb_arg eq_name functional_ref f_ref terminate_ref equation
(fun x ->
prove_eq (fun _ -> tclIDTAC)
{nb_arg=nb_arg;
- f_terminate = EConstr.of_constr (constr_of_global terminate_ref);
+ f_terminate = EConstr.of_constr (constr_of_monomorphic_global terminate_ref);
f_constr = EConstr.of_constr f_constr;
concl_tac = tclIDTAC;
func=functional_ref;
info=(instantiate_lambda Evd.empty
- (EConstr.of_constr (def_of_const (constr_of_global functional_ref)))
+ (EConstr.of_constr (def_of_const (constr_of_monomorphic_global functional_ref)))
(EConstr.of_constr f_constr::List.map mkVar x)
);
is_main_branch = true;
@@ -1570,9 +1570,9 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
if not stop
then
let eq_ref = Nametab.locate (qualid_of_ident equation_id ) in
- let f_ref = destConst (constr_of_global f_ref)
- and functional_ref = destConst (constr_of_global functional_ref)
- and eq_ref = destConst (constr_of_global eq_ref) in
+ let f_ref = destConst (constr_of_monomorphic_global f_ref)
+ and functional_ref = destConst (constr_of_monomorphic_global functional_ref)
+ and eq_ref = destConst (constr_of_monomorphic_global eq_ref) in
generate_induction_principle f_ref tcc_lemma_constr
functional_ref eq_ref rec_arg_num
(EConstr.of_constr rec_arg_type)
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index ef6af16036..de9dec0f74 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -207,7 +207,7 @@ struct
* ZMicromega.v
*)
- let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.gen_reference_in_modules s m n)
+ let gen_constant_in_modules s m n = EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.gen_reference_in_modules s m n)
let init_constant = gen_constant_in_modules "ZMicromega" Coqlib.init_modules
[@@@ocaml.warning "+3"]
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index e349031952..93c0d5c236 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -446,7 +446,7 @@ let lz_setoid_relation =
| Some (env', srel) when env' == env -> srel
| _ ->
let srel =
- try Some (UnivGen.constr_of_global @@
+ try Some (UnivGen.constr_of_monomorphic_global @@
Coqlib.find_reference "Class_setoid" ("Coq"::sdir) "RewriteRelation" [@ocaml.warning "-3"])
with _ -> None in
last_srel := Some (env, srel); srel
@@ -491,7 +491,7 @@ let rwprocess_rule dir rule gl =
| _ ->
let sigma, pi2 = Evd.fresh_global env sigma coq_prod.Coqlib.proj2 in
EConstr.mkApp (pi2, ra), sigma in
- if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_global @@ Coqlib.(lib_ref "core.True.type"))) then
+ if EConstr.eq_constr sigma a.(0) (EConstr.of_constr (UnivGen.constr_of_monomorphic_global @@ Coqlib.(lib_ref "core.True.type"))) then
let s, sigma = sr sigma 2 in
loop (converse_dir d) sigma s a.(1) rs 0
else
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 075ebf006a..0a5c85f4ab 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -290,7 +290,7 @@ let finalize_view s0 ?(simple_types=true) p =
Goal.enter_one ~__LOC__ begin fun g ->
let env = Goal.env g in
let sigma = Goal.sigma g in
- let evars_of_p = Evd.evars_of_term (EConstr.to_constr ~abort_on_undefined_evars:false sigma p) in
+ let evars_of_p = Evd.evars_of_term sigma p in
let filter x _ = Evar.Set.mem x evars_of_p in
let sigma = Typeclasses.resolve_typeclasses ~fail:false ~filter env sigma in
let p = Reductionops.nf_evar sigma p in
@@ -307,7 +307,7 @@ Goal.enter_one ~__LOC__ begin fun g ->
let und0 = (* Unassigned evars in the initial goal *)
let sigma0 = Tacmach.project s0 in
let g0info = Evd.find sigma0 (Tacmach.sig_it s0) in
- let g0 = Evd.evars_of_filtered_evar_info g0info in
+ let g0 = Evd.evars_of_filtered_evar_info sigma0 g0info in
List.filter (fun k -> Evar.Set.mem k g0)
(List.map fst (Evar.Map.bindings (Evd.undefined_map sigma0))) in
let rigid = rigid_of und0 in
diff --git a/plugins/ssrmatching/ssrmatching.ml b/plugins/ssrmatching/ssrmatching.ml
index 4e0866a0c5..adbcfb8f3b 100644
--- a/plugins/ssrmatching/ssrmatching.ml
+++ b/plugins/ssrmatching/ssrmatching.ml
@@ -529,8 +529,8 @@ exception FoundUnif of (evar_map * UState.t * tpattern)
(* Note: we don't update env as we descend into the term, as the primitive *)
(* unification procedure always rejects subterms with bound variables. *)
-let dont_impact_evars_in cl =
- let evs_in_cl = Evd.evars_of_term cl in
+let dont_impact_evars_in sigma0 cl =
+ let evs_in_cl = Evd.evars_of_term sigma0 cl in
fun sigma -> Evar.Set.for_all (fun k ->
try let _ = Evd.find_undefined sigma k in true
with Not_found -> false) evs_in_cl
@@ -544,7 +544,7 @@ let dont_impact_evars_in cl =
(* - w_unify expands let-in (zeta conversion) eagerly, whereas we want to *)
(* match a head let rigidly. *)
let match_upats_FO upats env sigma0 ise orig_c =
- let dont_impact_evars = dont_impact_evars_in orig_c in
+ let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr orig_c) in
let rec loop c =
let f, a = splay_app ise c in let i0 = ref (-1) in
let fpats =
@@ -586,7 +586,7 @@ let match_upats_FO upats env sigma0 ise orig_c =
let match_upats_HO ~on_instance upats env sigma0 ise c =
- let dont_impact_evars = dont_impact_evars_in c in
+ let dont_impact_evars = dont_impact_evars_in sigma0 (EConstr.of_constr c) in
let it_did_match = ref false in
let failed_because_of_TC = ref false in
let rec aux upats env sigma0 ise c =
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-30 11:56:34 +0000