aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--tactics/auto.ml9
-rw-r--r--tactics/autorewrite.ml13
-rw-r--r--tactics/contradiction.ml13
-rw-r--r--tactics/equality.ml18
-rw-r--r--tactics/evar_tactics.ml17
-rw-r--r--tactics/extratactics.ml411
-rw-r--r--tactics/inv.ml10
7 files changed, 54 insertions, 37 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 617c491c35..9ca6162a21 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -117,10 +117,11 @@ let exact poly (c,clenv) =
let ctx = Evd.evar_universe_context clenv.evd in
ctx, c
in
- Proofview.Goal.enter begin fun gl ->
- let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
- Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (exact_check c')
- end
+ Proofview.Goal.s_enter { enter = begin fun gl sigma ->
+ let sigma = Sigma.to_evar_map sigma in
+ let sigma = Evd.merge_universe_context sigma ctx in
+ Sigma.Unsafe.of_pair (exact_check c', sigma)
+ end }
(* Util *)
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 3a9d40de03..9892d29541 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -18,6 +18,8 @@ open Util
open Tacexpr
open Mod_subst
open Locus
+open Sigma.Notations
+open Proofview.Notations
(* Rewriting rules *)
type rew_rule = { rew_lemma: constr;
@@ -91,14 +93,15 @@ type raw_rew_rule = Loc.t * constr Univ.in_universe_context_set * bool * raw_tac
(* Applies all the rules of one base *)
let one_base general_rewrite_maybe_in tac_main bas =
let lrul = find_rewrites bas in
- let try_rewrite dir ctx c tc = Proofview.Goal.nf_enter (fun gl ->
+ let try_rewrite dir ctx c tc =
+ Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
let subst, ctx' = Universes.fresh_universe_context_set_instance ctx in
let c' = Vars.subst_univs_level_constr subst c in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Sigma.to_evar_map sigma in
let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx' in
- Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (general_rewrite_maybe_in dir c' tc)
- ) in
+ let tac = general_rewrite_maybe_in dir c' tc in
+ Sigma.Unsafe.of_pair (tac, sigma)
+ end } in
let lrul = List.map (fun h ->
let tac = match h.rew_tac with None -> Proofview.tclUNIT () | Some t -> Tacinterp.eval_tactic t in
(h.rew_ctx,h.rew_lemma,h.rew_l2r,tac)) lrul in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 22f218b4fb..0253747641 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -13,6 +13,8 @@ open Tactics
open Coqlib
open Reductionops
open Misctypes
+open Sigma.Notations
+open Proofview.Notations
(* Absurd *)
@@ -22,18 +24,19 @@ let mk_absurd_proof t =
mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
let absurd c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.s_enter { enter = begin fun gl sigma ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Sigma.to_evar_map sigma in
let j = Retyping.get_judgment_of env sigma c in
let sigma, j = Coercion.inh_coerce_to_sort Loc.ghost env sigma j in
let t = j.Environ.utj_val in
+ let tac =
Tacticals.New.tclTHENLIST [
- Proofview.Unsafe.tclEVARS sigma;
elim_type (build_coq_False ());
Simple.apply (mk_absurd_proof t)
- ]
- end
+ ] in
+ Sigma.Unsafe.of_pair (tac, sigma)
+ end }
let absurd c = absurd c
diff --git a/tactics/equality.ml b/tactics/equality.ml
index a74d555dd0..1f66699004 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -40,6 +40,7 @@ open Eqschemes
open Locus
open Locusops
open Misctypes
+open Sigma.Notations
open Proofview.Notations
open Unification
@@ -346,17 +347,20 @@ let type_of_clause cls gl = match cls with
| Some id -> pf_get_hyp_typ id gl
let leibniz_rewrite_ebindings_clause cls lft2rgt tac c t l with_evars frzevars dep_proof_ok hdcncl =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
let isatomic = isProd (whd_zeta hdcncl) in
let dep_fun = if isatomic then dependent else dependent_no_evar in
let type_of_cls = type_of_clause cls gl in
let dep = dep_proof_ok && dep_fun c type_of_cls in
let (sigma,elim,effs) = find_elim hdcncl lft2rgt dep cls (Some t) gl in
- Proofview.Unsafe.tclEVARS sigma <*> Proofview.tclEFFECTS effs <*>
+ let tac =
+ Proofview.tclEFFECTS effs <*>
general_elim_clause with_evars frzevars tac cls c t l
(match lft2rgt with None -> false | Some b -> b)
{elimindex = None; elimbody = (elim,NoBindings); elimrename = None}
- end
+ in
+ Sigma.Unsafe.of_pair (tac, sigma)
+ end }
let adjust_rewriting_direction args lft2rgt =
match args with
@@ -1472,19 +1476,21 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
(* on for further iterated sigma-tuples *)
let cutSubstInConcl l2r eqn =
- Proofview.Goal.nf_enter begin fun gl ->
+ Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_concl gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
let sigma,typ,expected = pf_apply subst_tuple_term gl e1 e2 typ in
+ let tac =
tclTHENFIRST
(tclTHENLIST [
- (Proofview.Unsafe.tclEVARS sigma);
(change_concl typ); (* Put in pattern form *)
(replace_core onConcl l2r eqn)
])
(change_concl expected) (* Put in normalized form *)
- end
+ in
+ Sigma.Unsafe.of_pair (tac, sigma)
+ end }
let cutSubstInHyp l2r eqn id =
Proofview.Goal.nf_enter begin fun gl ->
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 3d544274d2..43a31b04fc 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -15,6 +15,7 @@ open Refiner
open Evd
open Locus
open Sigma.Notations
+open Proofview.Notations
(* The instantiate tactic *)
@@ -69,17 +70,17 @@ let instantiate_tac_by_name id c =
let let_evar name typ =
let src = (Loc.ghost,Evar_kinds.GoalEvar) in
- Proofview.Goal.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ Proofview.Goal.s_enter { enter = begin fun gl sigma ->
let env = Proofview.Goal.env gl in
let id = match name with
| Names.Anonymous ->
let id = Namegen.id_of_name_using_hdchar env typ name in
Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
- | Names.Name id -> id in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma (evar, sigma', _) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
- let sigma' = Sigma.to_evar_map sigma' in
- Tacticals.New.tclTHEN (Proofview.V82.tactic (Refiner.tclEVARS sigma'))
+ | Names.Name id -> id
+ in
+ let Sigma (evar, sigma, p) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
+ let tac =
(Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
- end
+ in
+ Sigma (tac, sigma, p)
+ end }
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index d7d82111c8..f543a7691a 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -617,8 +617,8 @@ let out_arg = function
| ArgArg x -> x
let hResolve id c occ t =
- Proofview.Goal.nf_enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
let concl = Proofview.Goal.concl gl in
let env_ids = Termops.ids_of_context env in
@@ -636,10 +636,11 @@ let hResolve id c occ t =
let t_constr,ctx = resolve_hole (subst_var_with_hole occ id t_raw) in
let sigma = Evd.merge_universe_context sigma ctx in
let t_constr_type = Retyping.get_type_of env sigma t_constr in
- Tacticals.New.tclTHEN
- (Proofview.Unsafe.tclEVARS sigma)
+ let tac =
(change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))
- end
+ in
+ Sigma.Unsafe.of_pair (tac, sigma)
+ end }
let hResolve_auto id c t =
let rec resolve_auto n =
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 0acaeb44cf..85f2d2f91f 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -432,8 +432,8 @@ let rewrite_equations_tac as_mode othin id neqns names ba =
tac
let raw_inversion inv_kind id status names =
- Proofview.Goal.nf_enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ Proofview.Goal.nf_s_enter { enter = begin fun gl sigma ->
+ let sigma = Sigma.to_evar_map sigma in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
let c = mkVar id in
@@ -462,7 +462,7 @@ let raw_inversion inv_kind id status names =
in
let neqns = List.length realargs in
let as_mode = names != None in
- tclTHEN (Proofview.Unsafe.tclEVARS sigma)
+ let tac =
(tclTHENS
(assert_before Anonymous cut_concl)
[case_tac names
@@ -470,7 +470,9 @@ let raw_inversion inv_kind id status names =
(rewrite_equations_tac as_mode inv_kind id neqns))
(Some elim_predicate) ind (c, t);
onLastHypId (fun id -> tclTHEN (refined id) reflexivity)])
- end
+ in
+ Sigma.Unsafe.of_pair (tac, sigma)
+ end }
(* Error messages of the inversion tactics *)
let wrap_inv_error id = function (e, info) -> match e with
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:04:52 +0000