aboutsummaryrefslogtreecommitdiff
path: root/plugins
diff options
context:
space:
mode:
Diffstat (limited to 'plugins')
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/decl_mode/decl_proof_instr.ml4
-rw-r--r--plugins/firstorder/instances.ml7
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/funind/functional_principles_proofs.ml12
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--plugins/funind/invfun.ml26
-rw-r--r--plugins/funind/recdef.ml23
-rw-r--r--plugins/micromega/coq_micromega.ml2
-rw-r--r--plugins/omega/coq_omega.ml46
-rw-r--r--plugins/romega/refl_omega.ml2
-rw-r--r--plugins/setoid_ring/newring.ml12
13 files changed, 73 insertions, 71 deletions
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 5a49fc8f45..57eb80f5fb 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -250,7 +250,7 @@ module Btauto = struct
Tacticals.New.tclTHENLIST [
Tactics.change_concl changed_gl;
Tactics.apply (Lazy.force soundness);
- Proofview.V82.tactic (Tactics.normalise_vm_in_concl);
+ Tactics.normalise_vm_in_concl;
try_unification env
]
| _ ->
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index e5b68af8e8..b52f156a1b 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -48,7 +48,7 @@ let whd_delta env=
(* decompose member of equality in an applicative format *)
(** FIXME: evar leak *)
-let sf_of env sigma c = sort_of env (ref sigma) c
+let sf_of env sigma c = e_sort_of env (ref sigma) c
let rec decompose_term env sigma t=
match kind_of_term (whd env t) with
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 22a646b3f8..adfcb3e60d 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -407,7 +407,7 @@ let concl_refiner metas body gls =
let concl = pf_concl gls in
let evd = sig_sig gls in
let env = pf_env gls in
- let sort = family_of_sort (Typing.sort_of env (ref evd) concl) in
+ let sort = family_of_sort (Typing.e_sort_of env (ref evd) concl) in
let rec aux env avoid subst = function
[] -> anomaly ~label:"concl_refiner" (Pp.str "cannot happen")
| (n,typ)::rest ->
@@ -415,7 +415,7 @@ let concl_refiner metas body gls =
let x = id_of_name_using_hdchar env _A Anonymous in
let _x = fresh_id avoid x gls in
let nenv = Environ.push_named (LocalAssum (_x,_A)) env in
- let asort = family_of_sort (Typing.sort_of nenv (ref evd) _A) in
+ let asort = family_of_sort (Typing.e_sort_of nenv (ref evd) _A) in
let nsubst = (n,mkVar _x)::subst in
if List.is_empty rest then
asort,_A,mkNamedLambda _x _A (subst_meta nsubst body)
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 797f43f2a0..0bc40136c5 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -22,6 +22,7 @@ open Formula
open Sequent
open Names
open Misctypes
+open Sigma.Notations
open Context.Rel.Declaration
let compare_instance inst1 inst2=
@@ -117,8 +118,10 @@ let mk_open_instance id idc gl m t=
let rec aux n avoid env evmap decls =
if Int.equal n 0 then evmap, decls else
let nid=(fresh_id avoid var_id gl) in
- let evmap, (c, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
- let decl = LocalAssum (Name nid,c) in
+ let evmap = Sigma.Unsafe.of_evar_map evmap in
+ let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+ let evmap = Sigma.to_evar_map evmap in
+ let decl = LocalAssum (Name nid, c) in
aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m [] env evmap [] in
evmap, decls, revt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index b0e8f7d25c..c05015c538 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -212,6 +212,6 @@ let defined_connectives=lazy
let normalize_evaluables=
onAllHypsAndConcl
(function
- None->unfold_in_concl (Lazy.force defined_connectives)
+ None-> Proofview.V82.of_tactic (unfold_in_concl (Lazy.force defined_connectives))
| Some id ->
- unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly))
+ Proofview.V82.of_tactic (unfold_in_hyp (Lazy.force defined_connectives) (id,InHypTypeOnly)))
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 28982c37fe..c8f8a19e5b 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -372,12 +372,12 @@ let isLetIn t =
| _ -> false
-let h_reduce_with_zeta =
- reduce
+let h_reduce_with_zeta cl =
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
- })
+ }) cl)
@@ -708,7 +708,7 @@ let build_proof
[
generalize (term_eq::(List.map mkVar dyn_infos.rec_hyps));
thin dyn_infos.rec_hyps;
- pattern_option [Locus.AllOccurrencesBut [1],t] None;
+ Proofview.V82.of_tactic (pattern_option [Locus.AllOccurrencesBut [1],t] None);
(fun g -> observe_tac "toto" (
tclTHENSEQ [Proofview.V82.of_tactic (Simple.case t);
(fun g' ->
@@ -1338,7 +1338,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let fname = destConst (fst (decompose_app (List.hd (List.rev pte_args)))) in
tclTHENSEQ
- [unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))];
+ [Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst fname))]);
let do_prove =
build_proof
interactive_proof
@@ -1464,7 +1464,7 @@ let new_prove_with_tcc is_mes acc_inv hrec tcc_hyps eqs : tactic =
(fun g ->
if is_mes
then
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))] g
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference (delayed_force ltof_ref))]) g
else tclIDTAC g
);
observe_tac "rew_and_finish"
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 86abf9e2ef..84a4d910ef 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -114,7 +114,7 @@ let functional_induction with_clean c princl pat =
in
Tacticals.tclTHEN
(Tacticals.tclMAP (fun id -> Tacticals.tclTRY (Proofview.V82.of_tactic (Equality.subst_gen (do_rewrite_dependent ()) [id]))) idl )
- (Tactics.reduce flag Locusops.allHypsAndConcl)
+ (Proofview.V82.of_tactic (Tactics.reduce flag Locusops.allHypsAndConcl))
g
else Tacticals.tclIDTAC g
in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 56bc4328d1..cdb9c5067f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -368,14 +368,14 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
(* unfolding of all the defined variables introduced by this branch *)
(* observe_tac "unfolding" pre_tac; *)
(* $zeta$ normalizing of the conclusion *)
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{ Redops.all_flags with
Genredexpr.rDelta = false ;
Genredexpr.rConst = []
}
)
- Locusops.onConcl;
+ Locusops.onConcl);
observe_tac ("toto ") tclIDTAC;
(* introducing the the result of the graph and the equality hypothesis *)
@@ -490,15 +490,15 @@ and intros_with_rewrite_aux : tactic =
tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g))
then tclTHENSEQ[
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))];
- tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) ))
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]);
+ tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )))
(pf_ids_of_hyps g);
intros_with_rewrite
] g
else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g))
then tclTHENSEQ[
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))];
- tclMAP (fun id -> tclTRY(unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) ))
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]);
+ tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )))
(pf_ids_of_hyps g);
intros_with_rewrite
] g
@@ -538,12 +538,12 @@ and intros_with_rewrite_aux : tactic =
] g
| LetIn _ ->
tclTHENSEQ[
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
})
- Locusops.onConcl
+ Locusops.onConcl)
;
intros_with_rewrite
] g
@@ -553,12 +553,12 @@ and intros_with_rewrite_aux : tactic =
end
| LetIn _ ->
tclTHENSEQ[
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
})
- Locusops.onConcl
+ Locusops.onConcl)
;
intros_with_rewrite
] g
@@ -698,18 +698,18 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
(* Don't forget to $\zeta$ normlize the term since the principles
have been $\zeta$-normalized *)
- reduce
+ Proofview.V82.of_tactic (reduce
(Genredexpr.Cbv
{Redops.all_flags
with Genredexpr.rDelta = false;
})
- Locusops.onConcl
+ Locusops.onConcl)
;
generalize (List.map mkVar ids);
thin ids
]
else
- unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))]
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))])
in
(* The proof of each branche itself *)
let ind_number = ref 0 in
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 09c5aa5673..046c7aa437 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -276,8 +276,8 @@ let tclUSER tac is_mes l g =
if is_mes
then observe_tclTHENLIST (str "tclUSER2")
[
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
- (delayed_force Indfun_common.ltof_ref))];
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference
+ (delayed_force Indfun_common.ltof_ref))]);
tac
]
else tac
@@ -562,10 +562,10 @@ let rec destruct_bounds_aux infos (bound,hyple,rechyps) lbounds g =
observe_tclTHENLIST (str "destruct_bounds_aux2")[
observe_tac (str "clearing k ") (clear [id]);
h_intros [k;h';def];
- observe_tac (str "simple_iter") (simpl_iter Locusops.onConcl);
+ observe_tac (str "simple_iter") (Proofview.V82.of_tactic (simpl_iter Locusops.onConcl));
observe_tac (str "unfold functional")
- (unfold_in_concl[(Locus.OnlyOccurrences [1],
- evaluable_of_global_reference infos.func)]);
+ (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+ evaluable_of_global_reference infos.func)]));
(
observe_tclTHENLIST (str "test")[
list_rewrite true
@@ -692,9 +692,8 @@ let mkDestructEq :
[generalize new_hyps;
(fun g2 ->
let changefun patvars = { run = fun sigma ->
- let sigma = Sigma.to_evar_map sigma in
- let (sigma, c) = pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2) in
- Sigma.Unsafe.of_pair (c, sigma)
+ let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
+ redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
} in
Proofview.V82.of_tactic (change_in_concl None changefun) g2);
Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -904,10 +903,10 @@ let make_rewrite expr_info l hp max =
[observe_tac(str "make_rewrite finalize") (
(* tclORELSE( h_reflexivity) *)
(observe_tclTHENLIST (str "make_rewrite")[
- simpl_iter Locusops.onConcl;
+ Proofview.V82.of_tactic (simpl_iter Locusops.onConcl);
observe_tac (str "unfold functional")
- (unfold_in_concl[(Locus.OnlyOccurrences [1],
- evaluable_of_global_reference expr_info.func)]);
+ (Proofview.V82.of_tactic (unfold_in_concl[(Locus.OnlyOccurrences [1],
+ evaluable_of_global_reference expr_info.func)]));
(list_rewrite true
(List.map (fun e -> mkVar e,true) expr_info.eqs));
@@ -1427,7 +1426,7 @@ let start_equation (f:global_reference) (term_f:global_reference)
let x = n_x_id ids nargs in
observe_tac (str "start_equation") (observe_tclTHENLIST (str "start_equation") [
h_intros x;
- unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)];
+ Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, evaluable_of_global_reference f)]);
observe_tac (str "simplest_case")
(Proofview.V82.of_tactic (simplest_case (mkApp (terminate_constr,
Array.of_list (List.map mkVar x)))));
diff --git a/plugins/micromega/coq_micromega.ml b/plugins/micromega/coq_micromega.ml
index 1dd53a3fd8..27daa7e3c6 100644
--- a/plugins/micromega/coq_micromega.ml
+++ b/plugins/micromega/coq_micromega.ml
@@ -1170,7 +1170,7 @@ struct
let is_prop term =
let ty = Typing.unsafe_type_of (Tacmach.pf_env gl) (Tacmach.project gl) term in
- let sort = Typing.sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
+ let sort = Typing.e_sort_of (Tacmach.pf_env gl) (ref (Tacmach.project gl)) ty in
Term.is_prop_sort sort in
let rec xparse_formula env tg term =
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index b740649e98..1f420cf6ae 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -928,15 +928,15 @@ let rec transform p t =
transform p
(mkApp (Lazy.force coq_Zplus,
[| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
- unfold sp_Zminus :: tac,t
+ Proofview.V82.of_tactic (unfold sp_Zminus) :: tac,t
| Kapp(Zsucc,[t1]) ->
let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
[| t1; mk_integer one |])) in
- unfold sp_Zsucc :: tac,t
+ Proofview.V82.of_tactic (unfold sp_Zsucc) :: tac,t
| Kapp(Zpred,[t1]) ->
let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
[| t1; mk_integer negone |])) in
- unfold sp_Zpred :: tac,t
+ Proofview.V82.of_tactic (unfold sp_Zpred) :: tac,t
| Kapp(Zmult,[t1;t2]) ->
let tac1,t1' = transform (P_APP 1 :: p) t1
and tac2,t2' = transform (P_APP 2 :: p) t2 in
@@ -1092,8 +1092,8 @@ let replay_history tactic_normalisation =
in
Tacticals.New.tclTHENS
(Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (unfold sp_Zle);
- Proofview.V82.tactic (simpl_in_concl);
+ unfold sp_Zle;
+ simpl_in_concl;
intro;
(absurd not_sup_sup) ])
[ assumption ; reflexivity ]
@@ -1136,10 +1136,10 @@ let replay_history tactic_normalisation =
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHENLIST [
- (Proofview.V82.tactic (unfold sp_Zgt));
- (Proofview.V82.tactic simpl_in_concl);
+ (unfold sp_Zgt);
+ simpl_in_concl;
reflexivity ] ];
- Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (unfold sp_Zgt); Proofview.V82.tactic simpl_in_concl; reflexivity ]
+ Tacticals.New.tclTHENLIST [ unfold sp_Zgt; simpl_in_concl; reflexivity ]
];
Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
@@ -1161,18 +1161,18 @@ let replay_history tactic_normalisation =
[mkApp (Lazy.force coq_OMEGA4,
[| dd;kk;eq2;mkVar aux1; mkVar aux2 |])]);
Proofview.V82.tactic (clear [aux1;aux2]);
- Proofview.V82.tactic (unfold sp_not);
+ unfold sp_not;
(intros_using [aux]);
Proofview.V82.tactic (resolve_id aux);
Proofview.V82.tactic (mk_then tac);
assumption ] ;
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (unfold sp_Zgt);
- Proofview.V82.tactic simpl_in_concl;
+ unfold sp_Zgt;
+ simpl_in_concl;
reflexivity ] ];
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (unfold sp_Zgt);
- Proofview.V82.tactic simpl_in_concl;
+ unfold sp_Zgt;
+ simpl_in_concl;
reflexivity ] ]
| EXACT_DIVIDE (e1,k) :: l ->
let id = hyp_of_tag e1.id in
@@ -1209,8 +1209,8 @@ let replay_history tactic_normalisation =
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (unfold sp_Zgt);
- Proofview.V82.tactic simpl_in_concl;
+ unfold sp_Zgt;
+ simpl_in_concl;
reflexivity ] ];
Tacticals.New.tclTHEN (Proofview.V82.tactic (mk_then tac)) reflexivity ]
| (MERGE_EQ(e3,e1,e2)) :: l ->
@@ -1330,12 +1330,12 @@ let replay_history tactic_normalisation =
(intros_using [id]);
(loop l) ];
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (unfold sp_Zgt);
- Proofview.V82.tactic simpl_in_concl;
+ unfold sp_Zgt;
+ simpl_in_concl;
reflexivity ] ];
Tacticals.New.tclTHENLIST [
- Proofview.V82.tactic (unfold sp_Zgt);
- Proofview.V82.tactic simpl_in_concl;
+ unfold sp_Zgt;
+ simpl_in_concl;
reflexivity ] ]
| CONSTANT_NOT_NUL(e,k) :: l ->
Tacticals.New.tclTHEN (Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)])) Equality.discrConcl
@@ -1344,9 +1344,9 @@ let replay_history tactic_normalisation =
| CONSTANT_NEG(e,k) :: l ->
Tacticals.New.tclTHENLIST [
Proofview.V82.tactic (generalize_tac [mkVar (hyp_of_tag e)]);
- Proofview.V82.tactic (unfold sp_Zle);
- Proofview.V82.tactic simpl_in_concl;
- Proofview.V82.tactic (unfold sp_not);
+ unfold sp_Zle;
+ simpl_in_concl;
+ unfold sp_not;
(intros_using [aux]);
Proofview.V82.tactic (resolve_id aux);
reflexivity
@@ -1838,7 +1838,7 @@ let destructure_goal =
match destructurate_prop t with
| Kapp(Not,[t]) ->
(Tacticals.New.tclTHEN
- (Tacticals.New.tclTHEN (Proofview.V82.tactic (unfold sp_not)) intro)
+ (Tacticals.New.tclTHEN (unfold sp_not) intro)
destructure_hyps)
| Kimp(a,b) -> (Tacticals.New.tclTHEN intro (loop b))
| Kapp(False,[]) -> destructure_hyps
diff --git a/plugins/romega/refl_omega.ml b/plugins/romega/refl_omega.ml
index 560e6a899e..177c870b3c 100644
--- a/plugins/romega/refl_omega.ml
+++ b/plugins/romega/refl_omega.ml
@@ -1285,7 +1285,7 @@ let resolution env full_reified_goal systems_list =
Proofview.V82.of_tactic (Tactics.change_concl reified) >>
Proofview.V82.of_tactic (Tactics.apply (app coq_do_omega [|decompose_tactic; normalization_trace|])) >>
show_goal >>
- Tactics.normalise_vm_in_concl >>
+ Proofview.V82.of_tactic (Tactics.normalise_vm_in_concl) >>
(*i Alternatives to the previous line:
- Normalisation without VM:
Tactics.normalise_in_concl
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e203b9f651..a67cc7cb87 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -99,10 +99,10 @@ let protect_red map env sigma c =
(mk_clos_but (lookup_map map c) (Esubst.subs_id 0) c);;
let protect_tac map =
- Tactics.reduct_option (protect_red map,DEFAULTcast) None ;;
+ Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) None);;
let protect_tac_in map id =
- Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp));;
+ Proofview.V82.of_tactic (Tactics.reduct_option (protect_red map,DEFAULTcast) (Some(id, Locus.InHyp)));;
(****************************************************************************)
@@ -527,8 +527,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
match opp with
Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
| None -> plapp evd coq_eq_smorph [|r;add;mul|] in
- let setoid = Typing.solve_evars env evd setoid in
- let op_morph = Typing.solve_evars env evd op_morph in
+ let setoid = Typing.e_solve_evars env evd setoid in
+ let op_morph = Typing.e_solve_evars env evd op_morph in
(setoid,op_morph)
| _ ->
let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -627,7 +627,7 @@ let make_hyp_list env evd lH =
(fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
(plapp evd coq_nil [|carrier|])
in
- let l' = Typing.solve_evars env evd l in
+ let l' = Typing.e_solve_evars env evd l in
Evarutil.nf_evars_universes !evd l'
let interp_power env evd pow =
@@ -753,7 +753,7 @@ let make_term_list env evd carrier rl =
let l = List.fold_right
(fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
(plapp evd coq_nil [|carrier|])
- in Typing.solve_evars env evd l
+ in Typing.e_solve_evars env evd l
let carg = Tacinterp.Value.of_constr
let tacarg expr =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-02 16:55:35 +0000