aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--plugins/cc/cctac.ml2
-rw-r--r--plugins/quote/quote.ml2
-rw-r--r--plugins/setoid_ring/newring.ml4
-rw-r--r--proofs/clenvtac.ml2
-rw-r--r--proofs/proofview.ml3
-rw-r--r--proofs/proofview.mli2
-rw-r--r--proofs/tacmach.ml12
-rw-r--r--proofs/tacmach.mli1
-rw-r--r--tactics/auto.ml16
-rw-r--r--tactics/contradiction.ml4
-rw-r--r--tactics/eauto.ml44
-rw-r--r--tactics/elim.ml2
-rw-r--r--tactics/equality.ml22
-rw-r--r--tactics/extratactics.ml44
-rw-r--r--tactics/rewrite.ml4
-rw-r--r--tactics/tacinterp.ml80
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml58
18 files changed, 115 insertions, 109 deletions
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 35178aa1e..8c15f54af 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -385,7 +385,7 @@ let discriminate_tac (cstr,u as cstru) p =
let identity = Universes.constr_of_global (Lazy.force _I) in
(* let trivial=pf_unsafe_type_of gls identity in *)
let trivial = Universes.constr_of_global (Lazy.force _True) in
- let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Proofview.Goal.sigma gl) in
+ let evm, outtype = Evd.new_sort_variable Evd.univ_flexible (Tacmach.New.project gl) in
let outtype = mkSort outtype in
let pred=mkLambda(Name xid,outtype,mkRel 1) in
let hid = Tacmach.New.of_old (pf_get_new_id (Id.of_string "Heq")) gl in
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 8d60b8ba2..04936cd83 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -228,7 +228,7 @@ let compute_ivs f cs gl =
let (args3, body3) = decompose_lam body2 in
let nargs3 = List.length args3 in
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let is_conv = Reductionops.is_conv env sigma in
begin match decomp_term body3 with
| Case(_,p,c,lci) -> (* <p> Case c of c1 ... cn end *)
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 8ff4230e8..dbe7710eb 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -749,7 +749,7 @@ let ltac_ring_structure e =
let ring_lookup (f:glob_tactic_expr) lH rl t =
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
try (* find_ring_strucure can raise an exception *)
let evdref = ref sigma in
@@ -1021,7 +1021,7 @@ let ltac_field_structure e =
let field_lookup (f:glob_tactic_expr) lH rl t =
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
try
let evdref = ref sigma in
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 65bd32536..894b290f1 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -121,7 +121,7 @@ let unify ?(flags=fail_quick_unif_flags) m =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
let n = Tacmach.New.pf_nf_concl gl in
- let evd = clear_metas (Proofview.Goal.sigma gl) in
+ let evd = clear_metas (Tacmach.New.project gl) in
try
let evd' = w_unify env evd CONV ~flags m n in
Proofview.Unsafe.tclEVARSADVANCE evd'
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 826b4772a..bded518e7 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -921,7 +921,7 @@ module Goal = struct
let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t)
let env { env=env } = env
- let sigma { sigma=sigma } = sigma
+ let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma
let hyps { env=env } = Environ.named_context env
let concl { concl=concl } = concl
let extra { sigma=sigma; self=self } = Goal.V82.extra sigma self
@@ -1061,6 +1061,7 @@ struct
let refine ?(unsafe = true) f = Goal.enter { Goal.enter = begin fun gl ->
let sigma = Goal.sigma gl in
+ let sigma = Sigma.to_evar_map sigma in
let env = Goal.env gl in
let concl = Goal.concl gl in
(** Save the [future_goals] state to restore them after the
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index 5c97ada34..0b6c147f9 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -444,7 +444,7 @@ module Goal : sig
val concl : ([ `NF ], 'r) t -> Term.constr
val hyps : ([ `NF ], 'r) t -> Context.named_context
val env : ('a, 'r) t -> Environ.env
- val sigma : ('a, 'r) t -> Evd.evar_map
+ val sigma : ('a, 'r) t -> 'r Sigma.t
val extra : ('a, 'r) t -> Evd.Store.t
(** Returns the goal's conclusion even if the goal is not
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 8af28b6ab..57c60cbee 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -158,11 +158,15 @@ let pr_glls glls =
(* Variants of [Tacmach] functions built with the new proof engine *)
module New = struct
+ let project gl =
+ let sigma = Proofview.Goal.sigma gl in
+ Sigma.to_evar_map sigma
+
let pf_apply f gl =
- f (Proofview.Goal.env gl) (Proofview.Goal.sigma gl)
+ f (Proofview.Goal.env gl) (project gl)
let of_old f gl =
- f { Evd.it = Proofview.Goal.goal gl ; sigma = Proofview.Goal.sigma gl }
+ f { Evd.it = Proofview.Goal.goal gl ; sigma = project gl; }
let pf_global id gl =
(** We only check for the existence of an [id] in [hyps] *)
@@ -216,7 +220,7 @@ module New = struct
(** We normalize the conclusion just after *)
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = project gl in
nf_evar sigma concl
let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
@@ -235,6 +239,6 @@ module New = struct
let pf_whd_betadeltaiota gl t = pf_apply whd_betadeltaiota gl t
let pf_compute gl t = pf_apply compute gl t
- let pf_nf_evar gl t = nf_evar (Proofview.Goal.sigma gl) t
+ let pf_nf_evar gl t = nf_evar (project gl) t
end
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 3ed6a2eeb..c45fd250c 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -111,6 +111,7 @@ module New : sig
(** FIXME: encapsulate the level in an existential type. *)
val of_old : (Proof_type.goal Evd.sigma -> 'a) -> ([ `NF ], 'r) Proofview.Goal.t -> 'a
+ val project : ('a, 'r) Proofview.Goal.t -> Evd.evar_map
val pf_env : ('a, 'r) Proofview.Goal.t -> Environ.env
val pf_concl : ([ `NF ], 'r) Proofview.Goal.t -> types
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 4e4eafe4e..4a520612f 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -76,7 +76,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
(** [clenv] has been generated by a hint-making function, so the only relevant
data in its evarmap is the set of metas. The [evar_reset_evd] function
below just replaces the metas of sigma by those coming from the clenv. *)
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let evd = Evd.evars_reset_evd ~with_conv_pbs:true ~with_univs:false sigma clenv.evd in
(** Still, we need to update the universes *)
let clenv, c =
@@ -153,7 +153,7 @@ let conclPattern concl pat tac =
in
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
constr_bindings env sigma >>= fun constr_bindings ->
Hook.get forward_interp_tactic constr_bindings tac
end }
@@ -322,7 +322,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
Tacticals.New.tclTHEN (dbg_intro dbg)
( Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let nf c = Evarutil.nf_evar sigma c in
let decl = Tacmach.New.pf_last_hyp (Proofview.Goal.assume gl) in
@@ -417,7 +417,7 @@ and trivial_resolve dbg mod_delta db_list local_db cl =
let trivial ?(debug=Off) lems dbnames =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let db_list = make_db_list dbnames in
let d = mk_trivial_dbg debug in
let hints = make_local_hint_db env sigma false lems in
@@ -428,7 +428,7 @@ let trivial ?(debug=Off) lems dbnames =
let full_trivial ?(debug=Off) lems =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let db_list = current_pure_db () in
let d = mk_trivial_dbg debug in
let hints = make_local_hint_db env sigma false lems in
@@ -459,7 +459,7 @@ let possible_resolve dbg mod_delta db_list local_db cl =
let extend_local_db decl db gl =
let env = Tacmach.New.pf_env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
Hint_db.add_list env sigma (make_resolve_hyp env sigma decl) db
(* Introduce an hypothesis, then call the continuation tactic [kont]
@@ -500,7 +500,7 @@ let default_search_depth = ref 5
let delta_auto debug mod_delta n lems dbnames =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let db_list = make_db_list dbnames in
let d = mk_auto_dbg debug in
let hints = make_local_hint_db env sigma false lems in
@@ -523,7 +523,7 @@ let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let db_list = current_pure_db () in
let d = mk_auto_dbg debug in
let hints = make_local_hint_db env sigma false lems in
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 34886d74d..0cc74ff44 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -55,7 +55,7 @@ let filter_hyp f tac =
let contradiction_context =
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let rec seek_neg l = match l with
| [] -> Tacticals.New.tclZEROMSG (Pp.str"No such contradiction")
@@ -91,7 +91,7 @@ let is_negation_of env sigma typ t =
let contradiction_term (c,lbind as cl) =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_unsafe_type_of gl in
let typ = type_of c in
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index 08502e0cc..dbdfb3e92 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -154,8 +154,8 @@ let e_exact poly flags (c,clenv) =
let rec e_trivial_fail_db db_list local_db =
let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
let d = Tacmach.New.pf_last_hyp gl in
- let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) d in
- e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) hintl local_db)
+ let hintl = make_resolve_hyp (Tacmach.New.pf_env gl) (Tacmach.New.project gl) d in
+ e_trivial_fail_db db_list (Hint_db.add_list (Tacmach.New.pf_env gl) (Tacmach.New.project gl) hintl local_db)
end } in
Proofview.Goal.enter { enter = begin fun gl ->
let tacl =
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 27e96637d..d3aa16092 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -97,7 +97,7 @@ let general_decompose recognizer c =
let head_in indl t gl =
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
try
let ity,_ =
if !up_to_delta
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 0c487c4e6..85bc50216 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -159,7 +159,7 @@ let instantiate_lemma_all frzevars gl c ty l l2r concl =
let try_occ (evd', c') =
Clenvtac.clenv_pose_dependent_evars true {eqclause with evd = evd'}
in
- let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_unif_flags eqclause in
+ let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_unif_flags eqclause in
let occs =
w_unify_to_subterm_all ~flags env eqclause.evd
((if l2r then c1 else c2),concl)
@@ -208,7 +208,7 @@ let rewrite_conv_closed_unif_flags = {
let rewrite_elim with_evars frzevars cls c e =
Proofview.Goal.enter { enter = begin fun gl ->
- let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
+ let flags = make_flags frzevars (Tacmach.New.project gl) rewrite_conv_closed_unif_flags c in
general_elim_clause with_evars flags cls c e
end }
@@ -276,7 +276,7 @@ let jmeq_same_dom gl = function
let rels, t = decompose_prod_assum t in
let env = Environ.push_rel_context rels (Proofview.Goal.env gl) in
match decompose_app t with
- | _, [dom1; _; dom2;_] -> is_conv env (Proofview.Goal.sigma gl) dom1 dom2
+ | _, [dom1; _; dom2;_] -> is_conv env (Tacmach.New.project gl) dom1 dom2
| _ -> false
(* find_elim determines which elimination principle is necessary to
@@ -317,7 +317,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
Logic.eq or Jmeq just before *)
assert false
in
- let sigma, elim = Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c) in
+ let sigma, elim = Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c) in
sigma, elim, Declareops.no_seff
else
let scheme_name = match dep, lft2rgt, inccl with
@@ -337,7 +337,7 @@ let find_elim hdcncl lft2rgt dep cls ot gl =
let c, eff = find_scheme scheme_name ind in
(* MS: cannot use pf_constr_of_global as the eliminator might be generated by side-effect *)
let sigma, elim =
- Evd.fresh_global (Global.env ()) (Proofview.Goal.sigma gl) (ConstRef c)
+ Evd.fresh_global (Global.env ()) (Tacmach.New.project gl) (ConstRef c)
in
sigma, elim, eff
| _ -> assert false
@@ -384,7 +384,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let ctype = get_type_of env sigma c in
let rels, t = decompose_prod_assum (whd_betaiotazeta sigma ctype) in
@@ -484,7 +484,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
let apply_special_clear_request clear_flag f =
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
try
let ((c, bl), sigma) = run_delayed env sigma f in
@@ -496,7 +496,7 @@ let apply_special_clear_request clear_flag f =
let general_multi_rewrite with_evars l cl tac =
let do1 l2r f =
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (c, sigma) = run_delayed env sigma f in
tclWITHHOLES with_evars
@@ -569,9 +569,9 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
let t1 = get_type_of c1
and t2 = get_type_of c2 in
let evd =
- if unsafe then Some (Proofview.Goal.sigma gl)
+ if unsafe then Some (Tacmach.New.project gl)
else
- try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Proofview.Goal.sigma gl))
+ try Some (Evarconv.the_conv_x (Proofview.Goal.env gl) t1 t2 (Tacmach.New.project gl))
with Evarconv.UnableToUnify _ -> None
in
match evd with
@@ -965,7 +965,7 @@ let onEquality with_evars tac (c,lbindc) =
let onNegatedEquality with_evars tac =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let ccl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
match kind_of_term (hnf_constr env sigma ccl) with
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index fa13234a6..e1997c705 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -664,7 +664,7 @@ END
let hget_evar n =
Proofview.Goal.nf_enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let evl = evar_list concl in
if List.length evl < n then
@@ -779,7 +779,7 @@ END
let eq_constr x y =
Proofview.Goal.enter { enter = begin fun gl ->
- let evd = Proofview.Goal.sigma gl in
+ let evd = Tacmach.New.project gl in
if Evarutil.eq_constr_univs_test evd evd x y then Proofview.tclUNIT ()
else Tacticals.New.tclFAIL 0 (str "Not equal")
end }
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 2667fa7ff..648d68f27 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1566,7 +1566,7 @@ let cl_rewrite_clause_newtac ?abs ?origsigma strat clause =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let ty = match clause with
| None -> concl
| Some id -> Environ.named_type id env
@@ -2040,7 +2040,7 @@ let not_declared env ty rel =
let setoid_proof ty fn fallback =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
Proofview.tclORELSE
begin
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 1ea19bce0..da3ab737b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -633,7 +633,7 @@ let pf_interp_constr ist gl =
let new_interp_constr ist c k =
let open Proofview in
Proofview.Goal.enter { enter = begin fun gl ->
- let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in
+ let (sigma, c) = interp_constr ist (Goal.env gl) (Tacmach.New.project gl) c in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma) (k c)
end }
@@ -790,11 +790,11 @@ let rec message_of_value v =
Ftactic.return (str "<tactic>")
else if has_type v (topwit wit_constr) then
let v = out_gen (topwit wit_constr) v in
- Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) v) end
+ Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) v) end
else if has_type v (topwit wit_constr_under_binders) then
let c = out_gen (topwit wit_constr_under_binders) v in
Ftactic.nf_enter begin fun gl ->
- Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Proofview.Goal.sigma gl) c)
+ Ftactic.return (pr_constr_under_binders_env (pf_env gl) (Tacmach.New.project gl) c)
end
else if has_type v (topwit wit_unit) then
Ftactic.return (str "()")
@@ -804,16 +804,16 @@ let rec message_of_value v =
let p = out_gen (topwit wit_intro_pattern) v in
let print env sigma c = pr_constr_env env sigma (fst (Tactics.run_delayed env Evd.empty c)) in
Ftactic.nf_enter begin fun gl ->
- Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Proofview.Goal.sigma gl) c) p)
+ Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env gl) (Tacmach.New.project gl) c) p)
end
else if has_type v (topwit wit_constr_context) then
let c = out_gen (topwit wit_constr_context) v in
- Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Proofview.Goal.sigma gl) c) end
+ Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) (Tacmach.New.project gl) c) end
else if has_type v (topwit wit_uconstr) then
let c = out_gen (topwit wit_uconstr) v in
Ftactic.nf_enter begin fun gl ->
Ftactic.return (pr_closed_glob_env (pf_env gl)
- (Proofview.Goal.sigma gl) c)
+ (Tacmach.New.project gl) c)
end
else match Value.to_list v with
| Some l ->
@@ -1224,7 +1224,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| BindingsArgType
| OptArgType _ | PairArgType _ -> (** generic handler *)
Ftactic.nf_enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
let goal = Proofview.Goal.goal gl in
@@ -1233,7 +1233,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
end
| _ as tag -> (** Special treatment. TODO: use generic handler *)
Ftactic.nf_enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
match tag with
| IntOrVarArgType ->
@@ -1352,7 +1352,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let ist = { ist with extra = TacStore.set ist.extra f_trace trace; } in
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let goal_sigma = Proofview.Goal.sigma gl in
+ let goal_sigma = Tacmach.New.project gl in
let concl = Proofview.Goal.concl gl in
let goal = Proofview.Goal.goal gl in
let tac = Tacenv.interp_ml_tactic opn in
@@ -1399,7 +1399,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
match arg with
| TacGeneric arg ->
Ftactic.nf_enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let goal = Proofview.Goal.goal gl in
let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return v)
@@ -1407,7 +1407,7 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
| Reference r -> interp_ltac_reference dloc false ist r
| ConstrMayEval c ->
Ftactic.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (sigma,c_interp) = interp_constr_may_eval ist env sigma c in
Ftactic.(lift (Proofview.Unsafe.tclEVARS sigma) <*> return (Value.of_constr c_interp))
@@ -1427,12 +1427,12 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
interp_app loc ist fv largs
| TacFreshId l ->
Ftactic.enter begin fun gl ->
- let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Proofview.Goal.sigma gl) l in
+ let id = interp_fresh_id ist (Tacmach.New.pf_env gl) (Tacmach.New.project gl) l in
Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id)))
end
| TacPretype c ->
Ftactic.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let {closure;term} = interp_uconstr ist env c in
let vars = {
@@ -1611,7 +1611,7 @@ and interp_match ist lz constr lmr =
end
end >>= fun constr ->
Ftactic.enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let ilr = read_match_rule (extract_ltac_constr_values ist env) ist env sigma lmr in
interp_match_successes lz ist (Tactic_matching.match_term env sigma constr ilr)
@@ -1620,7 +1620,7 @@ and interp_match ist lz constr lmr =
(* Interprets the Match Context expressions *)
and interp_match_goal ist lz lr lmr =
Ftactic.nf_enter begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let hyps = Proofview.Goal.hyps gl in
let hyps = if lr then List.rev hyps else hyps in
@@ -1767,7 +1767,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
end >>= fun result ->
Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let result = Value.normalize result in
try
let cresult = coerce_to_closed_constr env result in
@@ -1805,7 +1805,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacIntroPattern l ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
Tacticals.New.tclWITHHOLES false
(name_atomic ~env
@@ -1817,7 +1817,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacIntroMove (ido,hto) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let mloc = interp_move_location ist env sigma hto in
let ido = Option.map (interp_ident ist env sigma) ido in
name_atomic ~env
@@ -1840,7 +1840,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.Trace.name_tactic (fun () -> Pp.str"<apply>") begin
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let l = List.map (fun (k,c) ->
let loc, f = interp_open_constr_with_bindings_loc ist c in
(k,(loc,f))) cb
@@ -1856,7 +1856,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacElim (ev,(keep,cb),cbo) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
let sigma, cbo = Option.fold_map (interp_constr_with_bindings ist env) sigma cbo in
let named_tac =
@@ -1867,7 +1867,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end }
| TacCase (ev,(keep,cb)) ->
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
let named_tac =
@@ -1879,7 +1879,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacFix (idopt,n) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let idopt = Option.map (interp_ident ist env sigma) idopt in
name_atomic ~env
(TacFix(idopt,n))
@@ -1905,7 +1905,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacCofix idopt ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let idopt = Option.map (interp_ident ist env sigma) idopt in
name_atomic ~env
(TacCofix (idopt))
@@ -1931,7 +1931,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacAssert (b,t,ipat,c) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (sigma,c) =
(if Option.is_empty t then interp_constr else interp_type) ist env sigma c
in
@@ -1944,7 +1944,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end }
| TacGeneralize cl ->
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let sigma, cl = interp_constr_with_occurrences_and_name_as_list ist env sigma cl in
Tacticals.New.tclWITHHOLES false
@@ -1962,7 +1962,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.nf_evar_goals <*>
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let clp = interp_clause ist env sigma clp in
let eqpat = interp_intro_pattern_naming_option ist env sigma eqpat in
if Locusops.is_nowhere clp then
@@ -2005,7 +2005,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end;
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let lems = interp_auto_lemmas ist env sigma lems in
name_atomic ~env
(TacTrivial(debug,List.map snd lems,l))
@@ -2022,7 +2022,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end;
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let lems = interp_auto_lemmas ist env sigma lems in
name_atomic ~env
(TacAuto(debug,n,List.map snd lems,l))
@@ -2038,7 +2038,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.nf_evar_goals <*>
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let sigma,l =
List.fold_map begin fun sigma (c,(ipato,ipats),cls) ->
(* TODO: move sigma as a side-effect *)
@@ -2071,7 +2071,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacClear (b,l) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let l = interp_hyp_list ist env sigma l in
if b then name_atomic ~env (TacClear (b, l)) (Tactics.keep l)
else
@@ -2082,7 +2082,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacClearBody l ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let l = interp_hyp_list ist env sigma l in
name_atomic ~env
(TacClearBody l)
@@ -2097,7 +2097,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacRename l ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Tacmach.New.pf_env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let l =
List.map (fun (id1,id2) ->
interp_hyp ist env sigma id1,
@@ -2112,7 +2112,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacSplit (ev,bll) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
let named_tac =
let tac = Tactics.split_with_bindings ev bll in
@@ -2165,7 +2165,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.nf_evar_goals <*>
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
Proofview.V82.tactic begin fun gl ->
let (sigma,sign,op) = interp_typed_pattern ist env sigma op in
let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
@@ -2189,7 +2189,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacSymmetry c ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let cl = interp_clause ist env sigma c in
name_atomic ~env
(TacSymmetry cl)
@@ -2207,7 +2207,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
} in
(b,m,keep,f)) l in
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let cl = interp_clause ist env sigma cl in
name_atomic ~env
(TacRewrite (ev,l,cl,by))
@@ -2219,7 +2219,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInversion (DepInversion (k,c,ids),hyp) ->
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (sigma,c_interp) =
match c with
| None -> sigma , None
@@ -2239,7 +2239,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let hyps = interp_hyp_list ist env sigma idl in
let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
let sigma, ids_interp = interp_or_and_intro_pattern_option ist env sigma ids in
@@ -2251,7 +2251,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
| TacInversion (InversionUsing (c,idl),hyp) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (sigma,c_interp) = interp_constr ist env sigma c in
let dqhyps = interp_declared_or_quantified_hypothesis ist env sigma hyp in
let hyps = interp_hyp_list ist env sigma idl in
@@ -2413,7 +2413,7 @@ let dummy_id = Id.of_string "_"
let lift_constr_tac_to_ml_tac vars tac =
let tac _ ist = Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let map = function
| None -> None
| Some id ->
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index c67053252..bdbc0aa21 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -696,7 +696,7 @@ module New = struct
let pf_constr_of_global ref tac =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (sigma, c) = Evd.fresh_global env sigma ref in
Proofview.Unsafe.tclEVARS sigma <*> (tac c)
end }
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 66053a314..94e334914 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -187,7 +187,7 @@ let introduction ?(check=true) id =
Proofview.Goal.enter { enter = begin fun gl ->
let gl = Proofview.Goal.assume gl in
let concl = Proofview.Goal.concl gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let hyps = Proofview.Goal.hyps gl in
let store = Proofview.Goal.extra gl in
let env = Proofview.Goal.env gl in
@@ -226,7 +226,7 @@ let convert_concl ?(check=true) ty k =
let convert_hyp ?(check=true) d =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let ty = Proofview.Goal.raw_concl gl in
let store = Proofview.Goal.extra gl in
let sign = convert_hyp check (named_context_val env) sigma d in
@@ -401,7 +401,7 @@ let find_name mayrepl decl naming gl = match naming with
| NamingAvoid idl ->
(* this case must be compatible with [find_intro_names] below. *)
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
new_fresh_id idl (default_id env sigma decl) gl
| NamingBasedOn (id,idl) -> new_fresh_id idl id gl
| NamingMustBe (loc,id) ->
@@ -785,7 +785,7 @@ let build_intro_tac id dest tac = match dest with
let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
Proofview.Goal.enter { enter = begin fun gl ->
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
- let concl = nf_evar (Proofview.Goal.sigma gl) concl in
+ let concl = nf_evar (Tacmach.New.project gl) concl in
match kind_of_term concl with
| Prod (name,t,u) when not dep_flag || (dependent (mkRel 1) u) ->
let name = find_name false (name,None,t) name_flag gl in
@@ -999,7 +999,7 @@ let onOpenInductionArg env sigma tac = function
(Tacticals.New.onLastHyp
(fun c ->
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let pending = (sigma,sigma) in
tac clear_flag (pending,(c,NoBindings))
end }))
@@ -1008,7 +1008,7 @@ let onOpenInductionArg env sigma tac = function
Tacticals.New.tclTHEN
(try_intros_until_id_check id)
(Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let pending = (sigma,sigma) in
tac clear_flag (pending,(mkVar id,NoBindings))
end })
@@ -1038,7 +1038,7 @@ let map_induction_arg f = function
let cut c =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let concl = Tacmach.New.pf_nf_concl gl in
let is_sort =
try
@@ -1173,7 +1173,7 @@ let enforce_prop_bound_names rename tac =
let rename_branch i =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let t = Proofview.Goal.concl gl in
change_concl (aux env sigma i t)
end } in
@@ -1193,7 +1193,7 @@ let elimination_clause_scheme with_evars ?(with_classes=true) ?(flags=elim_flags
rename i (elim, elimty, bindings) indclause =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let elim = contract_letin_in_lam_header elim in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv =
@@ -1223,7 +1223,7 @@ type eliminator = {
let general_elim_clause_gen elimtac indclause elim =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (elimc,lbindelimc) = elim.elimbody in
let elimt = Retyping.get_type_of env sigma elimc in
let i =
@@ -1234,7 +1234,7 @@ let general_elim_clause_gen elimtac indclause elim =
let general_elim with_evars clear_flag (c, lbindc) elim =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let ct = Retyping.get_type_of env sigma c in
let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
let elimtac = elimination_clause_scheme with_evars in
@@ -1351,7 +1351,7 @@ let elimination_in_clause_scheme with_evars ?(flags=elim_flags ())
id rename i (elim, elimty, bindings) indclause =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let elim = contract_letin_in_lam_header elim in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
@@ -1429,7 +1429,7 @@ let make_projection env sigma params cstr sign elim i n c u =
let descend_in_conjunctions avoid tac (err, info) c =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
try
let t = Retyping.get_type_of env sigma c in
let ((ind,u),t) = reduce_to_quantified_ind env sigma t in
@@ -1450,7 +1450,7 @@ let descend_in_conjunctions avoid tac (err, info) c =
(List.init n (fun i ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
match make_projection env sigma params cstr sign elim i n c u with
| None -> Tacticals.New.tclFAIL 0 (mt())
| Some (p,pt) ->
@@ -1506,7 +1506,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
let rec try_main_apply with_destruct c =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let thm_ty0 = nf_betaiota sigma (Retyping.get_type_of env sigma c) in
let try_apply thm_ty nprod =
@@ -1578,7 +1578,7 @@ let rec apply_with_bindings_gen b e = function
let apply_with_delayed_bindings_gen b e l =
let one k (loc, f) =
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (cb, sigma) = run_delayed env sigma f in
Tacticals.New.tclWITHHOLES e
@@ -1648,7 +1648,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
id (clear_flag,(loc,(d,lbind))) tac =
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
let t' = Tacmach.New.pf_get_hyp_typ id gl in
@@ -1657,7 +1657,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let rec aux idstoclear with_destruct c =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
try
let clause = apply_in_once_main flags innerclause env sigma (c,lbind) in
clenv_refine_in ~sidecond_first with_evars targetid id sigma clause
@@ -1681,7 +1681,7 @@ let apply_in_delayed_once sidecond_first with_delta with_destruct with_evars nam
id (clear_flag,(loc,f)) tac =
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (c, sigma) = run_delayed env sigma f in
Tacticals.New.tclWITHHOLES with_evars
(apply_in_once sidecond_first with_delta with_destruct with_evars
@@ -1768,7 +1768,7 @@ let assumption =
else Tacticals.New.tclZEROMSG (str "No such assumption.")
| (id, c, t)::rest ->
let concl = Proofview.Goal.concl gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let (sigma, is_same_type) =
if only_eq then (sigma, Constr.equal t concl)
else
@@ -2244,7 +2244,7 @@ and intro_pattern_action loc b style pat thin destopt tac id = match pat with
else
Proofview.V82.tactic (clear [id]) in
Proofview.Goal.enter { enter = begin fun gl ->
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let env = Proofview.Goal.env gl in
let (c, sigma) = run_delayed env sigma f in
Tacticals.New.tclWITHHOLES false
@@ -3677,7 +3677,7 @@ let guess_elim isrec dep s hyp0 gl =
let given_elim hyp0 (elimc,lbind as e) gl =
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let ind_type_guess,_ = decompose_app ((strip_prod tmptyp0)) in
- Proofview.Goal.sigma gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
+ Tacmach.New.project gl, (e, Tacmach.New.pf_unsafe_type_of gl elimc), ind_type_guess
type scheme_signature =
(Id.t list * (elim_arg_kind * bool * Id.t) list) array
@@ -3722,7 +3722,7 @@ let is_functional_induction elimc gl =
let get_eliminator elim dep s gl = match elim with
| ElimUsing (elim,indsign) ->
- Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign
+ Tacmach.New.project gl, (* bugged, should be computed *) true, elim, indsign
| ElimOver (isrec,id) ->
let evd, (elimc,elimt),_ as elims = guess_elim isrec dep s id gl in
let _, (l, s) = compute_elim_signature elims id in
@@ -4023,7 +4023,7 @@ let induction_gen clear_flag isrec with_evars elim
| _ -> [] in
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let ccl = Proofview.Goal.raw_concl gl in
let cls = Option.default allHypsAndConcl cls in
let sigma = Sigma.Unsafe.of_evar_map sigma in
@@ -4112,7 +4112,7 @@ let induction_destruct isrec with_evars (lc,elim) =
| [c,(eqname,names as allnames),cls] ->
Proofview.Goal.nf_enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
match elim with
| Some elim when is_functional_induction elim gl ->
(* Standard induction on non-standard induction schemes *)
@@ -4139,7 +4139,7 @@ let induction_destruct isrec with_evars (lc,elim) =
| _ ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
match elim with
| None ->
(* Several arguments, without "using" clause *)
@@ -4155,7 +4155,7 @@ let induction_destruct isrec with_evars (lc,elim) =
(Tacticals.New.tclMAP (fun (a,b,cl) ->
Proofview.Goal.enter { enter = begin fun gl ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
onOpenInductionArg env sigma (fun clear_flag a ->
induction_gen clear_flag false with_evars None (a,b) cl) a
end }) l)
@@ -4267,7 +4267,7 @@ let (forward_setoid_reflexivity, setoid_reflexivity) = Hook.make ()
let maybe_betadeltaiota_concl allowred gl =
let concl = Tacmach.New.pf_nf_concl gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
if not allowred then concl
else
let env = Proofview.Goal.env gl in
@@ -4401,7 +4401,7 @@ let prove_transitivity hdcncl eq_kind t =
mkApp (hdcncl, [| typ; c1; t |]), mkApp (hdcncl, [| typ; t; c2 |])
| HeterogenousEq (typ1,c1,typ2,c2) ->
let env = Proofview.Goal.env gl in
- let sigma = Proofview.Goal.sigma gl in
+ let sigma = Tacmach.New.project gl in
let type_of = Typing.unsafe_type_of env sigma in
let typt = type_of t in
(mkApp(hdcncl, [| typ1; c1; typt ;t |]),
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 15:13:13 +0000