aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-06 17:09:51 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2014-09-06 17:24:39 +0200
commit521a7b96c8963428ca0ecb39a22f458bf603ccab (patch)
tree4b96ec735f49ef1867348170b7432f9c7adb28bf
parent3ea6d6888105edd5139ae0a4d8f8ecdb586aff6c (diff)
Renaming goal-entering functions.
1. Proofview.Goal.enter into Proofview.Goal.nf_enter. 2. Proofview.Goal.raw_enter into Proofview.Goal.enter. 3. Proofview.Goal.goals -> Proofview.Goals.nf_goals 4. Proofview.Goal.raw_goals -> Proofview.Goals.goals 5. Ftactic.goals -> Ftactic.nf_goals 6. Ftactic.raw_goals -> Ftactic.goals This is more uniform with the other functions of Coq.
Diffstat
-rw-r--r--grammar/tacextend.ml42
-rw-r--r--plugins/btauto/refl_btauto.ml4
-rw-r--r--plugins/cc/cctac.ml14
-rw-r--r--plugins/fourier/fourierR.ml2
-rw-r--r--plugins/omega/coq_omega.ml14
-rw-r--r--plugins/quote/quote.ml4
-rw-r--r--plugins/setoid_ring/newring.ml44
-rw-r--r--proofs/clenvtac.ml4
-rw-r--r--proofs/proofview.ml24
-rw-r--r--proofs/proofview.mli12
-rw-r--r--proofs/tactic_debug.ml2
-rw-r--r--tactics/auto.ml20
-rw-r--r--tactics/autorewrite.ml6
-rw-r--r--tactics/class_tactics.ml4
-rw-r--r--tactics/contradiction.ml10
-rw-r--r--tactics/elim.ml8
-rw-r--r--tactics/eqdecide.ml10
-rw-r--r--tactics/equality.ml46
-rw-r--r--tactics/evar_tactics.ml2
-rw-r--r--tactics/extratactics.ml418
-rw-r--r--tactics/ftactic.ml10
-rw-r--r--tactics/ftactic.mli4
-rw-r--r--tactics/inv.ml16
-rw-r--r--tactics/leminv.ml2
-rw-r--r--tactics/rewrite.ml10
-rw-r--r--tactics/tacinterp.ml88
-rw-r--r--tactics/tacticals.ml28
-rw-r--r--tactics/tactics.ml128
-rw-r--r--toplevel/auto_ind_decl.ml20
29 files changed, 258 insertions, 258 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4
index dd00bc19a..aec115b7e 100644
--- a/grammar/tacextend.ml4
+++ b/grammar/tacextend.ml4
@@ -189,7 +189,7 @@ let declare_tactic loc s c cl = match cl with
let name = mlexpr_of_string name in
let tac =
(** Special handling of tactics without arguments: such tactics do not do
- a Proofview.Goal.enter to compute their arguments. It matters for some
+ a Proofview.Goal.nf_enter to compute their arguments. It matters for some
whole-prof tactics like [shelve_unifiable]. *)
if List.is_empty rem then
<:expr< fun _ $lid:"ist"$ -> $tac$ >>
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index e6a841153..a28a46c74 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -216,7 +216,7 @@ module Btauto = struct
Tacticals.tclFAIL 0 msg gl
let try_unification env =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let eq = Lazy.force eq in
let t = decomp_term concl in
@@ -231,7 +231,7 @@ module Btauto = struct
end
let tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let eq = Lazy.force eq in
let bool = Lazy.force Bool.typ in
diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index e828345fa..45d6a9393 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -253,7 +253,7 @@ let new_app_global f args k =
let new_refine c = Proofview.V82.tactic (refine c)
let rec proof_tac p : unit Proofview.tactic =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let type_of t = Tacmach.New.pf_type_of gl t in
try (* type_of can raise exceptions *)
match p.p_rule with
@@ -321,7 +321,7 @@ let rec proof_tac p : unit Proofview.tactic =
end
let refute_tac c t1 t2 p =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let intype =
Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt1)) gl
@@ -338,7 +338,7 @@ let refine_exact_check c gl =
Tacticals.tclTHEN (Refiner.tclEVARS evm) (Proofview.V82.of_tactic (exact_check c)) gl
let convert_to_goal_tac c t1 t2 p =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let tt1=constr_of_term t1 and tt2=constr_of_term t2 in
let sort =
Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls tt2)) gl
@@ -353,7 +353,7 @@ let convert_to_goal_tac c t1 t2 p =
end
let convert_to_hyp_tac c1 t1 c2 t2 p =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let tt2=constr_of_term t2 in
let h = Tacmach.New.of_old (pf_get_new_id (Id.of_string "H")) gl in
let false_t=mkApp (c2,[|mkVar h|]) in
@@ -363,7 +363,7 @@ let convert_to_hyp_tac c1 t1 c2 t2 p =
end
let discriminate_tac (cstr,u as cstru) p =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let t1=constr_of_term p.p_lhs and t2=constr_of_term p.p_rhs in
let intype =
Tacmach.New.of_old (fun gls -> (* Termops.refresh_universes *) (pf_type_of gls t1)) gl
@@ -404,7 +404,7 @@ let build_term_to_complete uf meta pac =
applistc (mkConstructU cinfo.ci_constr) all_args
let cc_tactic depth additionnal_terms =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
Coqlib.check_required_library Coqlib.logic_module_name;
let _ = debug (Pp.str "Reading subgoal ...") in
let state = Tacmach.New.of_old (fun gls -> make_prb gls depth additionnal_terms) gl in
@@ -477,7 +477,7 @@ let congruence_tac depth l =
*)
let f_equal =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let type_of = Tacmach.New.pf_type_of gl in
let cut_eq c1 c2 =
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index a77b1d60a..551b210d3 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -463,7 +463,7 @@ exception GoalDone
(* Résolution d'inéquations linéaires dans R *)
let rec fourier () =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
Coqlib.check_required_library ["Coq";"fourier";"Fourier"];
let goal = strip_outer_cast concl in
diff --git a/plugins/omega/coq_omega.ml b/plugins/omega/coq_omega.ml
index 48c853029..f8fd71ae2 100644
--- a/plugins/omega/coq_omega.ml
+++ b/plugins/omega/coq_omega.ml
@@ -34,7 +34,7 @@ open OmegaSolver
(* Added by JCF, 09/03/98 *)
let elim_id id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
simplest_elim (Tacmach.New.pf_global id gl)
end
let resolve_id id gl = Proofview.V82.of_tactic (apply (pf_global gl id)) gl
@@ -1416,7 +1416,7 @@ let reintroduce id =
open Proofview.Notations
let coq_omega =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
clear_constr_tables ();
let hyps_types = Tacmach.New.pf_hyps_types gl in
let destructure_omega = Tacmach.New.of_old destructure_omega gl in
@@ -1469,7 +1469,7 @@ let coq_omega =
let coq_omega = coq_omega
let nat_inject =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let is_conv = Tacmach.New.pf_apply Reductionops.is_conv gl in
let rec explore p t : unit Proofview.tactic =
try match destructurate_term t with
@@ -1673,7 +1673,7 @@ let onClearedName id tac =
(* so renaming may be necessary *)
Tacticals.New.tclTHEN
(Proofview.V82.tactic (tclTRY (clear [id])))
- (Proofview.Goal.enter begin fun gl ->
+ (Proofview.Goal.nf_enter begin fun gl ->
let id = Tacmach.New.of_old (fresh_id [] id) gl in
Tacticals.New.tclTHEN (Proofview.V82.tactic (introduction id)) (tac id)
end)
@@ -1681,14 +1681,14 @@ let onClearedName id tac =
let onClearedName2 id tac =
Tacticals.New.tclTHEN
(Proofview.V82.tactic (tclTRY (clear [id])))
- (Proofview.Goal.enter begin fun gl ->
+ (Proofview.Goal.nf_enter begin fun gl ->
let id1 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_left")) gl in
let id2 = Tacmach.New.of_old (fresh_id [] (add_suffix id "_right")) gl in
Tacticals.New.tclTHENLIST [ Proofview.V82.tactic (introduction id1); Proofview.V82.tactic (introduction id2); tac id1 id2 ]
end)
let destructure_hyps =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let type_of = Tacmach.New.pf_type_of gl in
let decidability = Tacmach.New.of_old decidability gl in
let pf_nf = Tacmach.New.of_old pf_nf gl in
@@ -1831,7 +1831,7 @@ let destructure_hyps =
end
let destructure_goal =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let decidability = Tacmach.New.of_old decidability gl in
let rec loop t =
diff --git a/plugins/quote/quote.ml b/plugins/quote/quote.ml
index 7ed4a0dbc..745e190cb 100644
--- a/plugins/quote/quote.ml
+++ b/plugins/quote/quote.ml
@@ -446,7 +446,7 @@ let quote_terms ivs lc =
yet. *)
let quote f lid =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let f = Tacmach.New.pf_global f gl in
let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
let ivs = compute_ivs f cl gl in
@@ -462,7 +462,7 @@ let quote f lid =
end
let gen_quote cont c f lid =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let f = Tacmach.New.pf_global f gl in
let cl = List.map (fun id -> Tacmach.New.pf_global id gl) lid in
let ivs = compute_ivs f cl gl in
diff --git a/plugins/setoid_ring/newring.ml4 b/plugins/setoid_ring/newring.ml4
index 2647ca22a..97936991e 100644
--- a/plugins/setoid_ring/newring.ml4
+++ b/plugins/setoid_ring/newring.ml4
@@ -824,7 +824,7 @@ let ltac_ring_structure e =
lemma1;lemma2;pretac;posttac]
let ring_lookup (f:glob_tactic_expr) lH rl t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
try (* find_ring_strucure can raise an exception *)
@@ -1140,7 +1140,7 @@ let ltac_field_structure e =
field_simpl_eq_in_ok;cond_ok;pretac;posttac]
let field_lookup (f:glob_tactic_expr) lH rl t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
try
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 589cb5bda..d4826ce20 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -83,7 +83,7 @@ open Unification
let dft = default_unify_flags
let res_pf ?(with_evars=false) ?(flags=dft ()) clenv =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let clenv gl = clenv_unique_resolver ~flags clenv gl in
clenv_refine with_evars (Tacmach.New.of_old clenv (Proofview.Goal.assume gl))
end
@@ -112,7 +112,7 @@ let fail_quick_unif_flags = {
(* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
let unify ?(flags=fail_quick_unif_flags) m =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Tacmach.New.pf_env gl in
let n = Tacmach.New.pf_nf_concl gl in
let evd = create_goal_evar_defs (Proofview.Goal.sigma gl) in
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 506d04f38..48ca84891 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -848,40 +848,40 @@ module Goal = struct
let hyps { env=env } = Environ.named_context env
let concl { concl=concl } = concl
- let enter_t = Goal.nf_enter begin fun env sigma concl self ->
+ let nf_enter_t = Goal.nf_enter begin fun env sigma concl self ->
{env=env;sigma=sigma;concl=concl;self=self}
end
- let enter f =
+ let nf_enter f =
list_iter_goal () begin fun goal () ->
Proof.current >>= fun env ->
tclEVARMAP >>= fun sigma ->
try
- let (gl, sigma) = Goal.eval enter_t env sigma goal in
+ let (gl, sigma) = Goal.eval nf_enter_t env sigma goal in
tclTHEN (V82.tclEVARS sigma) (f gl)
with e when catchable_exception e ->
let e = Errors.push e in
tclZERO e
end
- let raw_enter_t f = Goal.enter begin fun env sigma concl self ->
+ let enter_t f = Goal.enter begin fun env sigma concl self ->
f {env=env;sigma=sigma;concl=concl;self=self}
end
- let raw_enter f =
+ let enter f =
list_iter_goal () begin fun goal () ->
Proof.current >>= fun env ->
tclEVARMAP >>= fun sigma ->
try
(* raw_enter_t cannot modify the sigma. *)
- let (t,_) = Goal.eval (raw_enter_t f) env sigma goal in
+ let (t,_) = Goal.eval (enter_t f) env sigma goal in
t
with e when catchable_exception e ->
let e = Errors.push e in
tclZERO e
end
- let goals =
+ let nf_goals =
Proof.current >>= fun env ->
Proof.get >>= fun step ->
let sigma = step.solution in
@@ -890,12 +890,12 @@ module Goal = struct
| None -> None (** ppedrot: Is this check really necessary? *)
| Some goal ->
(** The sigma is unchanged. *)
- let (gl, _) = Goal.eval enter_t env sigma goal in
+ let (gl, _) = Goal.eval nf_enter_t env sigma goal in
Some gl
in
tclUNIT (List.map_filter map step.comb)
- let raw_goals =
+ let goals =
Proof.current >>= fun env ->
Proof.get >>= fun step ->
let sigma = step.solution in
@@ -904,7 +904,7 @@ module Goal = struct
| None -> None (** ppedrot: Is this check really necessary? *)
| Some goal ->
(** The sigma is unchanged. *)
- let (gl, _) = Goal.eval (raw_enter_t (fun gl -> gl)) env sigma goal in
+ let (gl, _) = Goal.eval (enter_t (fun gl -> gl)) env sigma goal in
Some gl
in
tclUNIT (List.map_filter map step.comb)
@@ -963,7 +963,7 @@ struct
let () = Typing.check env evdref c concl in
!evdref
- let refine ?(unsafe = false) f = Goal.raw_enter begin fun gl ->
+ let refine ?(unsafe = false) f = Goal.enter begin fun gl ->
let sigma = Goal.sigma gl in
let env = Goal.env gl in
let concl = Goal.concl gl in
@@ -980,7 +980,7 @@ struct
Proof.set { solution = sigma; comb; }
end
- let refine_casted ?(unsafe = false) f = Goal.raw_enter begin fun gl ->
+ let refine_casted ?(unsafe = false) f = Goal.enter begin fun gl ->
let concl = Goal.concl gl in
let env = Goal.env gl in
let f h = let (h, c) = f h in with_type h env c concl in
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index b4a4a7197..72dcc8c37 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -394,19 +394,19 @@ module Goal : sig
val env : 'a t -> Environ.env
val sigma : 'a t -> Evd.evar_map
- (* [enter t] execute the goal-dependent tactic [t] in each goal
+ (* [nf_enter t] execute the goal-dependent tactic [t] in each goal
independently. In particular [t] need not backtrack the same way in
each goal. *)
- val enter : ([ `NF ] t -> unit tactic) -> unit tactic
+ val nf_enter : ([ `NF ] t -> unit tactic) -> unit tactic
- (** Same as enter, but does not normalize the goal beforehand. *)
- val raw_enter : ([ `LZ ] t -> unit tactic) -> unit tactic
+ (** Same as nf_enter, but does not normalize the goal beforehand. *)
+ val enter : ([ `LZ ] t -> unit tactic) -> unit tactic
(** Recover the list of current goals under focus *)
- val goals : [ `NF ] t list tactic
+ val nf_goals : [ `NF ] t list tactic
(** Recover the list of current goals under focus, without evar-normalization *)
- val raw_goals : [ `LZ ] t list tactic
+ val goals : [ `LZ ] t list tactic
(* compatibility: avoid if possible *)
val goal : [ `NF ] t -> Goal.goal
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 62b157307..19a1f7758 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -52,7 +52,7 @@ let db_pr_goal gl =
str" " ++ pc) ++ fnl ()
let db_pr_goal =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let pg = db_pr_goal gl in
Proofview.tclLIFT (msg_tac_debug (str "Goal:" ++ fnl () ++ pg))
end
diff --git a/tactics/auto.ml b/tactics/auto.ml
index 418fc62f0..d269bf02d 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -1158,7 +1158,7 @@ let exact poly (c,clenv) =
let ctx = Evd.evar_universe_context clenv.evd in
ctx, c
in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Evd.merge_universe_context (Proofview.Goal.sigma gl) ctx in
Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma) (exact_check c')
end
@@ -1227,7 +1227,7 @@ let conclPattern concl pat tac =
with ConstrMatching.PatternMatchingFailure ->
Proofview.tclZERO (UserError ("conclPattern",str"conclPattern"))
in
- Proofview.Goal.raw_enter (fun gl ->
+ Proofview.Goal.enter (fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
constr_bindings env sigma >>= fun constr_bindings ->
@@ -1391,7 +1391,7 @@ let dbg_assumption dbg = tclLOG dbg (fun () -> str "assumption") assumption
let rec trivial_fail_db dbg mod_delta db_list local_db =
let intro_tac =
Tacticals.New.tclTHEN (dbg_intro dbg)
- ( Proofview.Goal.raw_enter begin fun gl ->
+ ( Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let nf c = Evarutil.nf_evar sigma c in
@@ -1401,7 +1401,7 @@ let rec trivial_fail_db dbg mod_delta db_list local_db =
in trivial_fail_db dbg mod_delta db_list (Hint_db.add_list hintl local_db)
end)
in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
Tacticals.New.tclFIRST
((dbg_assumption dbg)::intro_tac::
@@ -1495,7 +1495,7 @@ let make_db_list dbnames =
List.map lookup dbnames
let trivial ?(debug=Off) lems dbnames =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let db_list = make_db_list dbnames in
let d = mk_trivial_dbg debug in
let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
@@ -1504,7 +1504,7 @@ let trivial ?(debug=Off) lems dbnames =
end
let full_trivial ?(debug=Off) lems =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let dbs = !searchtable in
let dbs = String.Map.remove "v62" dbs in
let db_list = List.map snd (String.Map.bindings dbs) in
@@ -1543,7 +1543,7 @@ let extend_local_db decl db gl =
let intro_register dbg kont db =
Tacticals.New.tclTHEN (dbg_intro dbg)
- (Proofview.Goal.raw_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let extend_local_db decl db = extend_local_db decl db gl in
Tacticals.New.onLastDecl (fun decl -> kont (extend_local_db decl db))
end)
@@ -1559,7 +1559,7 @@ let search d n mod_delta db_list local_db =
if Int.equal n 0 then Proofview.tclZERO (Errors.UserError ("",str"BOUND 2")) else
Tacticals.New.tclORELSE0 (dbg_assumption d)
(Tacticals.New.tclORELSE0 (intro_register d (search d n) local_db)
- ( Proofview.Goal.raw_enter begin fun gl ->
+ ( Proofview.Goal.enter begin fun gl ->
let concl = Tacmach.New.pf_nf_concl gl in
let d' = incr_dbg d in
Tacticals.New.tclFIRST
@@ -1574,7 +1574,7 @@ let search d n mod_delta db_list local_db =
let default_search_depth = ref 5
let delta_auto debug mod_delta n lems dbnames =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let db_list = make_db_list dbnames in
let d = mk_auto_dbg debug in
let hints = Tacmach.New.of_old (make_local_hint_db false lems) gl in
@@ -1595,7 +1595,7 @@ let new_auto ?(debug=Off) n = delta_auto debug true n
let default_auto = auto !default_search_depth [] []
let delta_full_auto ?(debug=Off) mod_delta n lems =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let dbs = !searchtable in
let dbs = String.Map.remove "v62" dbs in
let db_list = List.map snd (String.Map.bindings dbs) in
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 0809c0500..65166ec11 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -91,7 +91,7 @@ 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.enter (fun gl ->
+ let try_rewrite dir ctx c tc = Proofview.Goal.nf_enter (fun gl ->
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
@@ -120,7 +120,7 @@ let autorewrite ?(conds=Naive) tac_main lbas =
(Proofview.tclUNIT()) lbas))
let autorewrite_multi_in ?(conds=Naive) idl tac_main lbas =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
(* let's check at once if id exists (to raise the appropriate error) *)
let _ = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) idl in
let general_rewrite_in id =
@@ -188,7 +188,7 @@ let gen_auto_multi_rewrite conds tac_main lbas cl =
| None ->
(* try to rewrite in all hypothesis
(except maybe the rewritten one) *)
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let ids = Tacmach.New.pf_ids_of_hyps gl in
try_do_hyps (fun id -> id) ids
end)
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 1160884c3..c741610a3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -75,10 +75,10 @@ let rec eq_constr_mod_evars x y =
| _, _ -> compare_constr eq_constr_mod_evars x y
let progress_evars t =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let check =
- Proofview.Goal.enter begin fun gl' ->
+ Proofview.Goal.nf_enter begin fun gl' ->
let newconcl = Proofview.Goal.concl gl' in
if eq_constr_mod_evars concl newconcl
then Tacticals.New.tclFAIL 0 (str"No progress made (modulo evars)")
diff --git a/tactics/contradiction.ml b/tactics/contradiction.ml
index 4a43b8038..cb1b7d557 100644
--- a/tactics/contradiction.ml
+++ b/tactics/contradiction.ml
@@ -24,7 +24,7 @@ let mk_absurd_proof t =
mkLambda (Names.Name id,t,mkApp (mkRel 2,[|mkRel 1|])))
let absurd c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let j = Retyping.get_judgment_of env sigma c in
@@ -47,13 +47,13 @@ let filter_hyp f tac =
| [] -> Proofview.tclZERO Not_found
| (id,_,t)::rest when f t -> tac id
| _::rest -> seek rest in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
seek hyps
end
let contradiction_context =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let rec seek_neg l = match l with
@@ -66,7 +66,7 @@ let contradiction_context =
else match kind_of_term typ with
| Prod (na,t,u) when is_empty_type u ->
(Proofview.tclORELSE
- (Proofview.Goal.raw_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let is_conv_leq = Tacmach.New.pf_apply is_conv_leq gl in
filter_hyp (fun typ -> is_conv_leq typ t)
(fun id' -> simplest_elim (mkApp (mkVar id,[|mkVar id'|])))
@@ -89,7 +89,7 @@ let is_negation_of env sigma typ t =
| _ -> false
let contradiction_term (c,lbind as cl) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_type_of gl in
diff --git a/tactics/elim.ml b/tactics/elim.ml
index 2bedf2a4c..ba413d410 100644
--- a/tactics/elim.ml
+++ b/tactics/elim.ml
@@ -85,7 +85,7 @@ let tmphyp_name = Id.of_string "_TmpHyp"
let up_to_delta = ref false (* true *)
let general_decompose recognizer c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let type_of = pf_type_of gl in
let typc = type_of c in
tclTHENS (cut typc)
@@ -108,7 +108,7 @@ let head_in indl t gl =
with Not_found -> false
let decompose_these c l =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let indl = List.map (fun x -> x, Univ.Instance.empty) l in
general_decompose (fun (_,t) -> head_in indl t gl) c
end
@@ -139,7 +139,7 @@ let induction_trailer abs_i abs_j bargs =
(tclDO (abs_j - abs_i) intro)
(onLastHypId
(fun id ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let idty = pf_type_of gl (mkVar id) in
let fvty = global_vars (pf_env gl) idty in
let possible_bring_hyps =
@@ -161,7 +161,7 @@ let induction_trailer abs_i abs_j bargs =
))
let double_ind h1 h2 =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let abs_i = of_old (depth_of_quantified_hypothesis true h1) gl in
let abs_j = of_old (depth_of_quantified_hypothesis true h2) gl in
let abs =
diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index 1c249c999..a43e99a7f 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -132,7 +132,7 @@ let match_eqdec c =
(* /spiwack *)
let solveArg eqonleft op a1 a2 tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let rectype = pf_type_of gl a1 in
let decide = mkDecideEqGoal eqonleft op rectype a1 a2 in
let subtacs =
@@ -144,7 +144,7 @@ let solveArg eqonleft op a1 a2 tac =
let solveEqBranch rectype =
Proofview.tclORELSE
begin
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = pf_nf_concl gl in
match_eqdec concl >>= fun (eqonleft,op,lhs,rhs,_) ->
let (mib,mip) = Global.lookup_inductive rectype in
@@ -171,7 +171,7 @@ let hd_app c = match kind_of_term c with
let decideGralEquality =
Proofview.tclORELSE
begin
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = pf_nf_concl gl in
match_eqdec concl >>= fun (eqonleft,_,c1,c2,typ) ->
let headtyp = hd_app (pf_compute gl typ) in
@@ -193,7 +193,7 @@ let decideGralEquality =
let decideEqualityGoal = tclTHEN intros decideGralEquality
let decideEquality rectype =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let decide = mkGenDecideEqGoal rectype gl in
(tclTHENS (cut decide) [default_auto;decideEqualityGoal])
end
@@ -202,7 +202,7 @@ let decideEquality rectype =
(* The tactic Compare *)
let compare c1 c2 =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let rectype = pf_type_of gl c1 in
let decide = mkDecideEqGoal true (build_coq_sumbool ()) rectype c1 c2 in
(tclTHENS (cut decide)
diff --git a/tactics/equality.ml b/tactics/equality.ml
index beb0cfae8..de2609874 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -190,7 +190,7 @@ let rewrite_conv_closed_unif_flags = {
}
let rewrite_elim with_evars frzevars cls c e =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let flags = make_flags frzevars (Proofview.Goal.sigma gl) rewrite_conv_closed_unif_flags c in
general_elim_clause with_evars flags cls c e
end
@@ -228,7 +228,7 @@ let general_elim_clause with_evars frzevars tac cls c t l l2r elim =
(general_elim_clause with_evars frzevars cls c elim))
tac
in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let instantiate_lemma concl =
if not all then instantiate_lemma gl c t l l2r concl
else instantiate_lemma_all frzevars gl c t l l2r concl
@@ -328,7 +328,7 @@ 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.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
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
@@ -361,7 +361,7 @@ let general_rewrite_ebindings_clause cls lft2rgt occs frzevars dep_proof_ok ?tac
if occs != AllOccurrences then (
rewrite_side_tac (Hook.get forward_general_setoid_rewrite_clause cls lft2rgt occs (c,l) ~new_goals:[]) tac)
else
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let ctype = get_type_of env sigma c in
@@ -451,7 +451,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
let ids_of_hyps = pf_ids_of_hyps gl in
Id.Set.fold (fun id l -> List.remove Id.equal id l) ids_in_c ids_of_hyps
in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
do_hyps_atleastonce (ids gl)
end
in
@@ -461,7 +461,7 @@ let general_rewrite_clause l2r with_evars ?tac c cl =
do_hyps
let apply_special_clear_request clear_flag f =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
try
@@ -476,7 +476,7 @@ type delayed_open_constr_with_bindings =
let general_multi_rewrite with_evars l cl tac =
let do1 l2r f =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma,c = f env sigma in
@@ -545,7 +545,7 @@ let replace_using_leibniz clause c1 c2 l2r unsafe try_prove_eq_opt =
| None -> Proofview.tclUNIT ()
| Some tac -> tclCOMPLETE tac
in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let get_type_of = pf_apply get_type_of gl in
let t1 = get_type_of c1
and t2 = get_type_of c2 in
@@ -854,7 +854,7 @@ let rec build_discriminator sigma env dirn c sort = function
*)
let gen_absurdity id =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let hyp_typ = pf_get_hyp_typ id (Proofview.Goal.assume gl) in
let hyp_typ = pf_nf_evar gl hyp_typ in
if is_empty_type hyp_typ
@@ -918,7 +918,7 @@ let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn sort =
let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
let sigma = eq_clause.evd in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
match find_positions env sigma t1 t2 with
@@ -930,7 +930,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
end
let onEquality with_evars tac (c,lbindc) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let type_of = pf_type_of gl in
let reduce_to_quantified_ind = pf_apply Tacred.reduce_to_quantified_ind gl in
let t = type_of c in
@@ -945,7 +945,7 @@ let onEquality with_evars tac (c,lbindc) =
end
let onNegatedEquality with_evars tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let ccl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
@@ -1220,7 +1220,7 @@ let set_eq_dec_scheme_kind k = eq_dec_scheme_kind_name := (fun _ -> k)
let eqdep_dec = qualid_of_string "Coq.Logic.Eqdep_dec"
let inject_if_homogenous_dependent_pair ty =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
try
let eq,u,(t,t1,t2) = find_this_eq_data_decompose gl ty in
(* fetch the informations of the pair *)
@@ -1347,7 +1347,7 @@ let injConcl = injClause None false None
let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sort = pf_apply get_type_of gl (Proofview.Goal.concl gl) in
let sigma = clause.evd in
let env = Proofview.Goal.env gl in
@@ -1370,7 +1370,7 @@ let dEq with_evars =
(apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
let intro_decompe_eq tac data cl =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let cl = pf_apply make_clenv_binding gl cl NoBindings in
decompEqThen (fun _ -> tac) data cl
end
@@ -1458,7 +1458,7 @@ let subst_tuple_term env sigma dep_pair1 dep_pair2 b =
exception NothingToRewrite
let cutSubstInConcl l2r eqn =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
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
@@ -1473,7 +1473,7 @@ let cutSubstInConcl l2r eqn =
end
let cutSubstInHyp l2r eqn id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let (lbeq,u,(t,e1,e2)) = find_eq_data_decompose gl eqn in
let typ = pf_get_hyp_typ id gl in
let (e1,e2) = if l2r then (e1,e2) else (e2,e1) in
@@ -1510,7 +1510,7 @@ let cutRewriteInHyp l2r eqn id = cutRewriteClause l2r eqn (Some id)
let cutRewriteInConcl l2r eqn = cutRewriteClause l2r eqn None
let substClause l2r c cls =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let eq = pf_apply get_type_of gl c in
tclTHENS (cutSubstClause l2r eq cls)
[Proofview.tclUNIT (); Proofview.V82.tactic (exact_no_check c)]
@@ -1540,7 +1540,7 @@ user = raise user error specific to rewrite
(* Substitutions tactics (JCF) *)
let unfold_body x =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(** We normalize the given hypothesis immediately. *)
let hyps = Proofview.Goal.hyps (Proofview.Goal.assume gl) in
let (_, xval, _) = Context.lookup_named x hyps in
@@ -1580,7 +1580,7 @@ let is_eq_x gl x (id,_,c) =
erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one dep_proof_ok x (hyp,rhs,dir) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let hyps = Proofview.Goal.hyps gl in
let concl = Proofview.Goal.concl gl in
@@ -1612,7 +1612,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) =
it everywhere, and erase hyp and x; proceed by generalizing all dep hyps *)
let subst_one_var dep_proof_ok x =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let gl = Proofview.Goal.assume gl in
let (_,xval,_) = pf_get_hyp x gl in
(* If x has a body, simply replace x with body and clear x *)
@@ -1654,7 +1654,7 @@ let default_subst_tactic_flags () =
{ only_leibniz = true; rewrite_dependent_proof = false }
let subst_all ?(flags=default_subst_tactic_flags ()) () =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let find_eq_data_decompose = find_eq_data_decompose gl in
let test (_,c) =
try
@@ -1708,7 +1708,7 @@ let rewrite_assumption_cond cond_eq_term cl =
with | Failure _ | UserError _ -> arec rest gl
end
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
arec hyps gl
end
diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index ace595a7b..a98d2be0b 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -56,7 +56,7 @@ let instantiate_tac n (ist,rawc) ido =
let let_evar name typ =
let src = (Loc.ghost,Evar_kinds.GoalEvar) in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma',evar = Evarutil.new_evar sigma env ~src typ in
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index b71e51314..c90ec92d2 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -362,7 +362,7 @@ let refine_red_flags =
let refine_locs = { Locus.onhyps=None; concl_occs=Locus.AllOccurrences }
let refine_tac {Glob_term.closure=closure;term=term} =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let flags = Pretyping.all_no_fail_flags in
@@ -690,7 +690,7 @@ END
exception Found of unit Proofview.tactic
let rewrite_except h =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
Tacticals.New.tclMAP (fun id -> if Id.equal id h then Proofview.tclUNIT () else
Tacticals.New.tclTRY (Equality.general_rewrite_in true Locus.AllOccurrences true true id (mkVar h) false))
@@ -709,11 +709,11 @@ let refl_equal =
should be replaced by a call to the tactic but I don't know how to
call it before it is defined. *)
let mkCaseEq a : unit Proofview.tactic =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let type_of_a = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g a) gl in
Tacticals.New.tclTHENLIST
[Proofview.V82.tactic (Tactics.Simple.generalize [mkApp(delayed_force refl_equal, [| type_of_a; a|])]);
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
Proofview.V82.tactic begin
@@ -726,12 +726,12 @@ let mkCaseEq a : unit Proofview.tactic =
let case_eq_intros_rewrite x =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let n = nb_prod (Proofview.Goal.concl gl) in
(* Pp.msgnl (Printer.pr_lconstr x); *)
Tacticals.New.tclTHENLIST [
mkCaseEq x;
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let hyps = Tacmach.New.pf_ids_of_hyps gl in
let n' = nb_prod concl in
@@ -762,7 +762,7 @@ let destauto t =
with Found tac -> tac
let destauto_in id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let ctype = Tacmach.New.of_old (fun g -> Tacmach.pf_type_of g (mkVar id)) gl in
(* Pp.msgnl (Printer.pr_lconstr (mkVar id)); *)
(* Pp.msgnl (Printer.pr_lconstr (ctype)); *)
@@ -770,7 +770,7 @@ let destauto_in id =
end
TACTIC EXTEND destauto
-| [ "destauto" ] -> [ Proofview.Goal.enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
+| [ "destauto" ] -> [ Proofview.Goal.nf_enter (fun gl -> destauto (Proofview.Goal.concl gl)) ]
| [ "destauto" "in" hyp(id) ] -> [ destauto_in id ]
END
@@ -972,7 +972,7 @@ TACTIC EXTEND guard
END
let decompose l c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let to_ind c =
if isInd c then Univ.out_punivs (destInd c)
else error "not an inductive type"
diff --git a/tactics/ftactic.ml b/tactics/ftactic.ml
index fcc385c4e..bbc739a3b 100644
--- a/tactics/ftactic.ml
+++ b/tactics/ftactic.ml
@@ -29,7 +29,7 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
| Uniform x ->
(** We dispatch the uniform result on each goal under focus, as we know
that the [m] argument was actually dependent. *)
- Proofview.Goal.raw_goals >>= fun l ->
+ Proofview.Goal.goals >>= fun l ->
let ans = List.map (fun _ -> x) l in
Proofview.tclUNIT ans
| Depends l -> Proofview.tclUNIT l
@@ -37,12 +37,12 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function
Proofview.tclDISPATCHL (List.map f l) >>= fun l ->
Proofview.tclUNIT (Depends (List.concat l))
-let enter f =
- bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
+let nf_enter f =
+ bind (Proofview.Goal.nf_goals >>= fun l -> Proofview.tclUNIT (Depends l))
(fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
-let raw_enter f =
- bind (Proofview.Goal.raw_goals >>= fun l -> Proofview.tclUNIT (Depends l))
+let enter f =
+ bind (Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l))
(fun gl -> Proofview.V82.wrap_exceptions (fun () -> f gl))
let lift (type a) (t:a Proofview.tactic) : a t =
diff --git a/tactics/ftactic.mli b/tactics/ftactic.mli
index 16cfca08d..19ef717bc 100644
--- a/tactics/ftactic.mli
+++ b/tactics/ftactic.mli
@@ -37,10 +37,10 @@ val run : 'a t -> ('a -> unit Proofview.tactic) -> unit Proofview.tactic
(** {5 Focussing} *)
-val enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
+val nf_enter : ([ `NF ] Proofview.Goal.t -> 'a t) -> 'a t
(** Enter a goal. The resulting tactic is focussed. *)
-val raw_enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
+val enter : ([ `LZ ] Proofview.Goal.t -> 'a t) -> 'a t
(** Enter a goal, without evar normalization. The resulting tactic is
focussed. *)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 49a5bcd7e..c315cd560 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -268,7 +268,7 @@ Nota: with Inversion_clear, only four useless hypotheses
*)
let generalizeRewriteIntros tac depids id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let dids = dependent_hyps id depids gl in
(tclTHENLIST
[bring_hyps dids; tac;
@@ -298,7 +298,7 @@ let projectAndApply thin id eqname names depids =
(if thin then clear [id] else (remember_first_eq id eqname; tclIDTAC))
in
let substHypIfVariable tac id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
(** We only look at the type of hypothesis "id" *)
let hyp = pf_nf_evar gl (pf_get_hyp_typ id (Proofview.Goal.assume gl)) in
let (t,t1,t2) = Hipattern.dest_nf_eq gl hyp in
@@ -331,12 +331,12 @@ let projectAndApply thin id eqname names depids =
id
let nLastDecls i tac =
- Proofview.Goal.enter (fun gl -> tac (nLastDecls gl i))
+ Proofview.Goal.nf_enter (fun gl -> tac (nLastDecls gl i))
(* Inversion qui n'introduit pas les hypotheses, afin de pouvoir les nommer
soi-meme (proposition de Valerie). *)
let rewrite_equations_gene othin neqns ba =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
let rewrite_eqns =
match othin with
@@ -406,7 +406,7 @@ let extract_eqn_names = function
| Some x -> x
let rewrite_equations othin neqns names ba =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let names = List.map (get_names true) names in
let (depids,nodepids) = split_dep_and_nodep ba.Tacticals.assums gl in
let rewrite_eqns =
@@ -454,7 +454,7 @@ let rewrite_equations_tac (gene, othin) id neqns names ba =
let raw_inversion inv_kind id status names =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
@@ -531,12 +531,12 @@ let dinv_clear_tac id = dinv FullInversionClear None None (NamedHyp id)
* back to their places in the hyp-list. *)
let invIn k names ids id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
let concl = Proofview.Goal.concl gl in
let nb_prod_init = nb_prod concl in
let intros_replace_ids =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = pf_nf_concl gl in
let nb_of_new_hyp =
nb_prod concl - (List.length hyps + nb_prod_init)
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 237ce38b8..248acb8c8 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -266,7 +266,7 @@ let lemInv id c gls =
let lemInv_gen id c = try_intros_until (fun id -> Proofview.V82.tactic (lemInv id c)) id
let lemInvIn id c ids =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let hyps = List.map (fun id -> pf_get_hyp id gl) ids in
let intros_replace_ids =
let concl = Proofview.Goal.concl gl in
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index c545332ed..1d218572d 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -1464,7 +1464,7 @@ let cl_rewrite_clause_tac ?abs strat clause gl =
let new_refine (evd, c) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let update _ =
let evd = Evarconv.consider_remaining_unif_problems env evd in
@@ -1474,7 +1474,7 @@ let new_refine (evd, c) =
end
let assert_replacing id newt tac =
- let prf = Proofview.Goal.enter begin fun gl ->
+ let prf = Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let env = Proofview.Goal.env gl in
let nc' =
@@ -1516,7 +1516,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
| Some id, (undef, None, newt) ->
Proofview.V82.tactic (Tacmach.convert_hyp_no_check (id, None, newt))
| None, (undef, Some p, newt) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let make h =
let (h, ()) = Proofview.Refine.update h (fun _ -> undef, ()) in
@@ -1528,7 +1528,7 @@ let cl_rewrite_clause_newtac ?abs strat clause =
| None, (undef, None, newt) ->
Proofview.V82.tactic (Tacmach.convert_concl_no_check newt DEFAULTcast)
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_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
@@ -1986,7 +1986,7 @@ let not_declared env ty rel =
str ty ++ str" relation. Maybe you need to require the Setoid library")
let setoid_proof ty fn fallback =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index f4caefa70..5e4465213 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -583,7 +583,7 @@ let pf_interp_constr ist gl =
let new_interp_constr ist c k =
let open Proofview in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (sigma, c) = interp_constr ist (Goal.env gl) (Goal.sigma gl) c in
Proofview.tclTHEN (Proofview.V82.tclEVARS sigma) (k c)
end
@@ -726,10 +726,10 @@ 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.enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) v) end
+ Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env 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.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
Ftactic.return (pr_constr_under_binders_env (pf_env gl) c)
end
else if has_type v (topwit wit_unit) then
@@ -739,12 +739,12 @@ let rec message_of_value v =
else if has_type v (topwit wit_intro_pattern) then
let p = out_gen (topwit wit_intro_pattern) v in
let print env c = pr_constr_env env (snd (c env Evd.empty)) in
- Ftactic.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
Ftactic.return (Miscprint.pr_intro_pattern (fun c -> print (pf_env 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.enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) c) end
+ Ftactic.nf_enter begin fun gl -> Ftactic.return (pr_constr_env (pf_env gl) c) end
else match Value.to_list v with
| Some l ->
Ftactic.List.map message_of_value l >>= fun l ->
@@ -1074,7 +1074,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
tclSHOWHYPS (Proofview.V82.of_tactic (interp_tactic ist tac))
end
| TacAbstract (tac,ido) ->
- Proofview.Goal.enter begin fun gl -> Tactics.tclABSTRACT
+ Proofview.Goal.nf_enter begin fun gl -> Tactics.tclABSTRACT
(Option.map (Tacmach.New.of_old (pf_interp_ident ist) gl) ido) (interp_tactic ist tac)
end
| TacThen (t1,t) ->
@@ -1119,7 +1119,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| ConstrWithBindingsArgType
| BindingsArgType
| OptArgType _ | PairArgType _ -> (** generic handler *)
- Ftactic.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl gl in
@@ -1128,7 +1128,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
Ftactic.(lift (Proofview.V82.tclEVARS sigma) <*> return arg)
end
| _ as tag -> (** Special treatment. TODO: use generic handler *)
- Ftactic.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
match tag with
@@ -1221,7 +1221,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
| TacML (loc,opn,l) when List.for_all global_genarg l ->
(* spiwack: a special case for tactics (from TACTIC EXTEND) when
every argument can be interpreted without a
- [Proofview.Goal.enter]. *)
+ [Proofview.Goal.nf_enter]. *)
let tac = Tacenv.interp_ml_tactic opn in
(* dummy values, will be ignored *)
let env = Environ.empty_env in
@@ -1232,7 +1232,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
tac args ist
| TacML (loc,opn,l) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let goal_sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
@@ -1277,7 +1277,7 @@ and interp_ltac_reference loc' mustbetac ist r : typed_generic_argument Ftactic.
and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
match arg with
| TacGeneric arg ->
- Ftactic.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let goal = Proofview.Goal.goal gl in
let (sigma,v) = Geninterp.generic_interp ist {Evd.it=goal;sigma} arg in
@@ -1285,14 +1285,14 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
end
| Reference r -> interp_ltac_reference dloc false ist r
| ConstrMayEval c ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let sigma = Proofview.Goal.sigma 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.V82.tclEVARS sigma) <*> return (Value.of_constr c_interp))
end
| UConstr c ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
Ftactic.return (Value.of_uconstr (interp_uconstr ist env c))
end
@@ -1309,12 +1309,12 @@ and interp_tacarg ist arg : typed_generic_argument Ftactic.t =
Ftactic.List.map (fun a -> interp_tacarg ist a) la >>= fun la_interp ->
interp_external loc ist com req la_interp
| TacFreshId l ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let id = interp_fresh_id ist (Tacmach.New.pf_env gl) l in
Ftactic.return (in_gen (topwit wit_intro_pattern) (dloc, IntroNaming (IntroIdentifier id)))
end
| TacPretype c ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let {closure;term} = interp_uconstr ist env c in
@@ -1491,7 +1491,7 @@ and interp_match ist lz constr lmr =
Proofview.tclZERO e
end
end >>= fun constr ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let sigma = Proofview.Goal.sigma 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
@@ -1500,7 +1500,7 @@ and interp_match ist lz constr lmr =
(* Interprets the Match Context expressions *)
and interp_match_goal ist lz lr lmr =
- Ftactic.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let hyps = Proofview.Goal.hyps gl in
@@ -1511,7 +1511,7 @@ and interp_match_goal ist lz lr lmr =
end
and interp_external loc ist com req la =
- Ftactic.enter begin fun gl ->
+ Ftactic.nf_enter begin fun gl ->
let f ch = Tacmach.New.of_old (fun gl -> extern_request ch req gl la) gl in
let g ch = internalise_tacarg ch in
interp_tacarg ist (System.connect f g com)
@@ -1641,7 +1641,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
(val_interp ist e)
begin function
| Not_found ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
Proofview.tclLIFT begin
debugging_step ist (fun () ->
@@ -1653,7 +1653,7 @@ and interp_ltac_constr ist e : constr Ftactic.t =
| e -> Proofview.tclZERO e
end
end >>= fun result ->
- Ftactic.raw_enter begin fun gl ->
+ Ftactic.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let result = Value.normalize result in
try
@@ -1683,14 +1683,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
match tac with
(* Basic tactics *)
| TacIntroPattern l ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma,l' = interp_intro_pattern_list_as_list ist env sigma l in
Proofview.V82.tclEVARS sigma <*> Tactics.intros_patterns l'
end
| TacIntroMove (ido,hto) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let mloc = interp_move_location ist env hto in
Tactics.intro_move (Option.map (interp_fresh_ident ist env) ido) mloc
@@ -1704,7 +1704,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
gl
end
| TacApply (a,ev,cb,cl) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, l =
@@ -1718,7 +1718,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclWITHHOLES ev tac sigma l
end
| TacElim (ev,(keep,cb),cbo) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
@@ -1726,14 +1726,14 @@ and interp_atomic ist tac : unit Proofview.tactic =
Tacticals.New.tclWITHHOLES ev (Tactics.elim ev keep cb) sigma cbo
end
| TacCase (ev,(keep,cb)) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma, cb = interp_constr_with_bindings ist env sigma cb in
Tacticals.New.tclWITHHOLES ev (Tactics.general_case_analysis ev keep) sigma cb
end
| TacFix (idopt,n) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
Proofview.V82.tactic (Tactics.fix (Option.map (interp_fresh_ident ist env) idopt) n)
end
@@ -1752,7 +1752,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
gl
end
| TacCofix idopt ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
Proofview.V82.tactic (Tactics.cofix (Option.map (interp_fresh_ident ist env) idopt))
end
@@ -1771,7 +1771,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
gl
end
| TacAssert (b,t,ipat,c) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma,c) =
@@ -1783,7 +1783,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacGeneralize cl ->
let tac arg = Proofview.V82.tactic (Tactics.Simple.generalize_gen arg) in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma 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
@@ -1794,7 +1794,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(fun c -> Proofview.V82.tactic (Tactics.generalize_dep c))
| TacLetTac (na,c,clp,b,eqpat) ->
Proofview.V82.nf_evar_goals <*>
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let clp = interp_clause ist env clp in
@@ -1824,7 +1824,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Automation tactics *)
| TacTrivial (debug,lems,l) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
Auto.h_trivial ~debug
@@ -1832,7 +1832,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(Option.map (List.map (interp_hint_base ist)) l)
end
| TacAuto (debug,n,lems,l) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
Auto.h_auto ~debug (Option.map (interp_int_or_var ist) n)
@@ -1845,7 +1845,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* spiwack: some unknown part of destruct needs the goal to be
prenormalised. *)
Proofview.V82.nf_evar_goals <*>
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma,l =
@@ -1874,7 +1874,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
if b then Tactics.keep l gl else Tactics.clear l gl
end
| TacClearBody l ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tactics.clear_body (interp_hyp_list ist (Tacmach.New.pf_env gl) l)
end
| TacMove (dep,id1,id2) ->
@@ -1894,7 +1894,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Constructors *)
| TacSplit (ev,bll) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let sigma, bll = List.fold_map (interp_bindings ist env) sigma bll in
@@ -1930,7 +1930,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
end
| TacChange (Some op,c,cl) ->
Proofview.V82.nf_evar_goals <*>
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
Proofview.V82.tactic begin fun gl ->
@@ -1949,7 +1949,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Equivalence relations *)
| TacSymmetry c ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let cl = interp_clause ist env c in
Tactics.intros_symmetry cl
@@ -1957,7 +1957,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
(* Equality and inversion *)
| TacRewrite (ev,l,cl,by) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let l = List.map (fun (b,m,(keep,c)) ->
let f env sigma = interp_open_constr_with_bindings ist env sigma c in
(b,m,keep,f)) l in
@@ -1969,7 +1969,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
by)
end
| TacInversion (DepInversion (k,c,ids),hyp) ->
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma,c_interp) =
@@ -1986,7 +1986,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.tclEVARS sigma <*> Inv.dinv k c_interp ids dqhyps
end
| TacInversion (NonDepInversion (k,idl,ids),hyp) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let hyps = interp_hyp_list ist env idl in
@@ -1995,7 +1995,7 @@ and interp_atomic ist tac : unit Proofview.tactic =
Proofview.V82.tclEVARS sigma <*> Inv.inv_clause k ids hyps dqhyps
end
| TacInversion (InversionUsing (c,idl),hyp) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma,c_interp) = interp_constr ist env sigma c in
@@ -2026,7 +2026,7 @@ let eval_tactic_ist ist t =
let interp_tac_gen lfun avoid_ids debug t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let extra = TacStore.set TacStore.empty f_debug debug in
let extra = TacStore.set extra f_avoid_ids avoid_ids in
@@ -2057,7 +2057,7 @@ let hide_interp global t ot =
Proofview.tclENV >>= fun env ->
hide_interp env
else
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
hide_interp (Proofview.Goal.env gl)
end
@@ -2173,7 +2173,7 @@ let _ = Hook.set Auto.extern_interp
let dummy_id = Id.of_string "_"
let lift_constr_tac_to_ml_tac vars tac =
- let tac _ ist = Proofview.Goal.raw_enter begin fun gl ->
+ let tac _ ist = Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let map = function
| None -> None
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index 50f51de21..7c11857ba 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -516,21 +516,21 @@ module New = struct
mkVar (nthHypId m gl)
let onNthHypId m tac =
- Proofview.Goal.raw_enter begin fun gl -> tac (nthHypId m gl) end
+ Proofview.Goal.enter begin fun gl -> tac (nthHypId m gl) end
let onNthHyp m tac =
- Proofview.Goal.raw_enter begin fun gl -> tac (nthHyp m gl) end
+ Proofview.Goal.enter begin fun gl -> tac (nthHyp m gl) end
let onLastHypId = onNthHypId 1
let onLastHyp = onNthHyp 1
let onNthDecl m tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
Proofview.tclUNIT (nthDecl m gl) >>= tac
end
let onLastDecl = onNthDecl 1
let ifOnHyp pred tac1 tac2 id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let typ = Tacmach.New.pf_get_hyp_typ id gl in
if pred (id,typ) then
tac1 id
@@ -538,10 +538,10 @@ module New = struct
tac2 id
end
- let onHyps find tac = Proofview.Goal.enter (fun gl -> tac (find gl))
+ let onHyps find tac = Proofview.Goal.nf_enter (fun gl -> tac (find gl))
let afterHyp id tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let hyps = Proofview.Goal.hyps gl in
let rem, _ = List.split_when (fun (hyp,_,_) -> Id.equal hyp id) hyps in
tac rem
@@ -552,17 +552,17 @@ module New = struct
None :: List.map Option.make hyps
let tryAllHyps tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclFIRST_PROGRESS_ON tac hyps
end
let tryAllHypsAndConcl tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
tclFIRST_PROGRESS_ON tac (fullGoal gl)
end
let onClause tac cl =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let hyps = Tacmach.New.pf_ids_of_hyps gl in
tclMAP tac (Locusops.simple_clause_of (fun () -> hyps) cl)
end
@@ -571,7 +571,7 @@ module New = struct
(* c should be of type A1->.. An->B with B an inductive definition *)
let general_elim_then_using mk_elim
isrec allnames tac predicate ind (c, t) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let indclause = Tacmach.New.of_old (fun gl -> mk_clenv_from gl (c, t)) gl in
(** FIXME: evar leak. *)
let sigma, elim = Tacmach.New.of_old (mk_elim ind) gl in
@@ -627,7 +627,7 @@ module New = struct
end
let elimination_then tac c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in
let isrec,mkelim =
match (Global.lookup_mind (fst (fst ind))).mind_record with
@@ -644,13 +644,13 @@ module New = struct
general_elim_then_using gl_make_case_nodep false
let elim_on_ba tac ba =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let branches = Tacmach.New.of_old (make_elim_branch_assumptions ba) gl in
tac branches
end
let case_on_ba tac ba =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let branches = Tacmach.New.of_old (make_case_branch_assumptions ba) gl in
tac branches
end
@@ -670,7 +670,7 @@ module New = struct
| Some id -> elimination_sort_of_hyp id gl
let pf_constr_of_global ref tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (sigma, c) = Evd.fresh_global env sigma ref in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e006404eb..b369e0fbe 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -140,7 +140,7 @@ let convert_concl = Tacmach.convert_concl
let convert_hyp = Tacmach.convert_hyp
let convert_gen pb x y =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
try
let sigma = Tacmach.New.pf_apply Evd.conversion gl pb x y in
Proofview.V82.tclEVARS sigma
@@ -264,7 +264,7 @@ let find_name mayrepl decl naming gl = match naming with
(**************************************************************)
let assert_before_then_gen b naming t tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let id = find_name b (Anonymous,None,t) naming gl in
Tacticals.New.tclTHENLAST
(Proofview.V82.tactic
@@ -282,7 +282,7 @@ let assert_before na = assert_before_gen false (naming_of_name na)
let assert_before_replacing id = assert_before_gen true (NamingMustBe (dloc,id))
let assert_after_then_gen b naming t tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let id = find_name b (Anonymous,None,t) naming gl in
Tacticals.New.tclTHENFIRST
(Proofview.V82.tactic
@@ -565,7 +565,7 @@ let build_intro_tac id dest tac = match dest with
| dest -> Tacticals.New.tclTHENLIST [Proofview.V82.tactic (introduction id); Proofview.V82.tactic (move_hyp true id dest); tac id]
let rec intro_then_gen name_flag move_flag force_flag dep_flag tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let concl = nf_evar (Proofview.Goal.sigma gl) concl in
match kind_of_term concl with
@@ -698,7 +698,7 @@ let depth_of_quantified_hypothesis red h gl =
str".")
let intros_until_gen red h =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in
Tacticals.New.tclDO n (if red then introf else intro)
end
@@ -764,7 +764,7 @@ let map_induction_arg f = function
(****************************************)
let cut c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Tacmach.New.pf_nf_concl gl in
@@ -897,7 +897,7 @@ let enforce_prop_bound_names rename tac =
mkLetIn (na,c,t,aux (push_rel (na,Some c,t) env) sigma (i-1) t')
| _ -> print_int i; Pp.msg (print_constr t); assert false in
let rename_branch i =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let t = Proofview.Goal.concl gl in
@@ -910,7 +910,7 @@ let enforce_prop_bound_names rename tac =
tac
let elimination_clause_scheme with_evars ?(flags=elim_flags ()) rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
@@ -939,7 +939,7 @@ type eliminator = {
}
let general_elim_clause_gen elimtac indclause elim =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let (elimc,lbindelimc) = elim.elimbody in
@@ -950,7 +950,7 @@ let general_elim_clause_gen elimtac indclause elim =
end
let general_elim with_evars clear_flag (c, lbindc) elim =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let ct = Retyping.get_type_of env sigma c in
@@ -965,7 +965,7 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
(* Case analysis tactics *)
let general_case_analysis_in_context with_evars clear_flag (c,lbindc) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let concl = Proofview.Goal.concl gl in
@@ -1014,7 +1014,7 @@ let find_eliminator c gl =
let default_elim with_evars clear_flag (c,_ as cx) =
Proofview.tclORELSE
- (Proofview.Goal.raw_enter begin fun gl ->
+ (Proofview.Goal.enter begin fun gl ->
let evd, elim = find_eliminator c gl in
Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd)
(general_elim with_evars clear_flag cx elim)
@@ -1062,7 +1062,7 @@ let clenv_fchain_in id ?(flags=elim_flags ()) mv elimclause hypclause =
raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
let elimination_in_clause_scheme with_evars ?(flags=elim_flags ()) id rename i (elim, elimty, bindings) indclause =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let elimclause = make_clenv_binding env sigma (elim, elimty) bindings in
@@ -1139,7 +1139,7 @@ let make_projection env sigma params cstr sign elim i n c u =
in elim
let descend_in_conjunctions avoid tac exit c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
try
@@ -1160,7 +1160,7 @@ let descend_in_conjunctions avoid tac exit c =
NotADefinedRecordUseScheme (snd elim) in
Tacticals.New.tclFIRST
(List.init n (fun i ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
match make_projection env sigma params cstr sign elim i n c u with
@@ -1181,7 +1181,7 @@ let descend_in_conjunctions avoid tac exit c =
(****************************************************)
let solve_remaining_apply_goals =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
if !apply_solve_class_goals then
try
let env = Proofview.Goal.env gl in
@@ -1198,7 +1198,7 @@ let solve_remaining_apply_goals =
end
let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind)) =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let concl = Proofview.Goal.concl gl in
let flags =
if with_delta then default_unify_flags () else default_no_delta_unify_flags () in
@@ -1207,7 +1207,7 @@ let general_apply with_delta with_destruct with_evars clear_flag (loc,(c,lbind))
step. *)
let concl_nprod = nb_prod concl in
let rec try_main_apply with_destruct c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
@@ -1329,7 +1329,7 @@ let apply_in_once_main flags innerclause env sigma (d,lbind) =
let apply_in_once sidecond_first with_delta with_destruct with_evars naming
id (clear_flag,(loc,(d,lbind))) tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
let flags = if with_delta then elim_flags () else elim_no_delta_flags () in
@@ -1337,7 +1337,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
let innerclause = mk_clenv_from_env env sigma (Some 0) (mkVar id,t') in
let targetid = find_name true (Anonymous,None,t') naming gl in
let rec aux idstoclear with_destruct c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let sigma = Proofview.Goal.sigma gl in
try
@@ -1377,7 +1377,7 @@ let apply_in_once sidecond_first with_delta with_destruct with_evars naming
*)
let cut_and_apply c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
match kind_of_term (Tacmach.New.pf_hnf_constr gl (Tacmach.New.pf_type_of gl c)) with
| Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
let concl = Proofview.Goal.concl gl in
@@ -1406,7 +1406,7 @@ let new_exact_no_check c =
Proofview.Refine.refine ~unsafe:true (fun h -> (h, c))
let exact_check c =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(** We do not need to normalize the goal because we just check convertibility *)
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let env = Proofview.Goal.env gl in
@@ -1452,7 +1452,7 @@ let assumption =
let hyps = Proofview.Goal.hyps gl in
arec gl true hyps
in
- Proofview.Goal.enter assumption_tac
+ Proofview.Goal.nf_enter assumption_tac
(*****************************************************************)
(* Modification of a local context *)
@@ -1481,7 +1481,7 @@ let check_is_type env ty msg =
msg e
let clear_body ids =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Proofview.Goal.concl (Proofview.Goal.assume gl) in
let ctx = named_context env in
@@ -1604,7 +1604,7 @@ let check_number_of_constructors expctdnumopt i nconstr =
if i > nconstr then error "Not enough constructors."
let constructor_tac with_evars expctdnumopt i lbind =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let cl = Tacmach.New.pf_nf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
@@ -1638,7 +1638,7 @@ let rec tclANY tac = function
let any_constructor with_evars tacopt =
let t = match tacopt with None -> Proofview.tclUNIT () | Some t -> t in
let tac i = Tacticals.New.tclTHEN (constructor_tac with_evars None i NoBindings) t in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let cl = Tacmach.New.pf_nf_concl gl in
let reduce_to_quantified_ind =
Tacmach.New.pf_apply Tacred.reduce_to_quantified_ind gl
@@ -1698,7 +1698,7 @@ let my_find_eq_data_decompose gl t =
-> raise ConstrMatching.PatternMatchingFailure
let intro_decomp_eq loc l thin tac id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_type_of gl c in
let _,t = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -1709,7 +1709,7 @@ let intro_decomp_eq loc l thin tac id =
end
let intro_or_and_pattern loc bracketed ll thin tac id =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let c = mkVar id in
let t = Tacmach.New.pf_type_of gl c in
let ((ind,u),t) = Tacmach.New.pf_reduce_to_quantified_ind gl t in
@@ -1732,7 +1732,7 @@ let rewrite_hyp assert_style l2r id =
if assert_style then
rew_on l2r allHypsAndConcl
else
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let type_of = Tacmach.New.pf_type_of gl in
let whd_betadeltaiota = Tacmach.New.pf_apply whd_betadeltaiota gl in
@@ -1861,7 +1861,7 @@ and intro_pattern_action loc b style pat thin tac id = match pat with
(tac thin None [])
| IntroApplyOn (f,(loc,pat)) ->
let naming,tac_ipat = prepare_intros_loc loc (IntroIdentifier id) pat in
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let sigma = Proofview.Goal.sigma gl in
let env = Proofview.Goal.env gl in
let sigma,c = f env sigma in
@@ -1984,7 +1984,7 @@ let decode_hyp = function
*)
let letin_tac_gen with_eq abs ty =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let env = Proofview.Goal.env gl in
let evd = Proofview.Goal.sigma gl in
let ccl = Proofview.Goal.concl gl in
@@ -2013,7 +2013,7 @@ let letin_tac_gen with_eq abs ty =
(Proofview.Goal.sigma gl, mkNamedLetIn id c t ccl, Proofview.tclUNIT ()) in
Tacticals.New.tclTHEN
(Proofview.V82.tclEVARUNIVCONTEXT ctx)
- (Proofview.Goal.enter (fun gl ->
+ (Proofview.Goal.nf_enter (fun gl ->
let (sigma,newcl,eq_tac) = eq_tac gl in
Tacticals.New.tclTHENLIST
[ Proofview.V82.tclEVARS sigma;
@@ -2033,7 +2033,7 @@ let letin_pat_tac with_eq name c occs =
let forward b usetac ipat c =
match usetac with
| None ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let t = Tacmach.New.pf_type_of gl c in
Tacticals.New.tclTHENFIRST (assert_as true ipat t) (Proofview.V82.tactic (exact_no_check c))
end
@@ -2066,7 +2066,7 @@ let apply_type hdcty argl gl =
let bring_hyps hyps =
if List.is_empty hyps then Tacticals.New.tclIDTAC
else
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Tacmach.New.pf_nf_concl gl in
let newcl = List.fold_right mkNamedProd_or_LetIn hyps concl in
@@ -2078,7 +2078,7 @@ let bring_hyps hyps =
end
let revert hyps =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let gl = Proofview.Goal.assume gl in
let ctx = List.map (fun id -> Tacmach.New.pf_get_hyp id gl) hyps in
(bring_hyps ctx) <*> (Proofview.V82.tactic (clear hyps))
@@ -2167,7 +2167,7 @@ let generalize_gen_let lconstr gl =
if Option.is_empty b then Some c else None) lconstr)) gl
let new_generalize_gen_let lconstr =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.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
@@ -2363,7 +2363,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
match ra with
| (RecArg,deprec,recvarname) ::
(IndArg,depind,hyprecname) :: ra' ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (recpat,names) = match names with
| [loc,IntroNaming (IntroIdentifier id) as pat] ->
let id' = next_ident_away (add_prefix "IH" id) avoid in
@@ -2371,7 +2371,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
| _ -> consume_pattern avoid (Name recvarname) deprec gl names in
let dest = get_recarg_dest dests in
safe_dest_intro_patterns avoid thin dest [recpat] (fun ids thin ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (hyprec,names) =
consume_pattern avoid (Name hyprecname) depind gl names
in
@@ -2380,7 +2380,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
end)
end
| (IndArg,dep,hyprecname) :: ra' ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(* Rem: does not happen in Coq schemes, only in user-defined schemes *)
let pat,names =
consume_pattern avoid (Name hyprecname) dep gl names in
@@ -2388,7 +2388,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
peel_tac ra' (update_dest dests ids) names thin)
end
| (RecArg,dep,recvarname) :: ra' ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (pat,names) =
consume_pattern avoid (Name recvarname) dep gl names in
let dest = get_recarg_dest dests in
@@ -2396,7 +2396,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
peel_tac ra' dests names thin)
end
| (OtherArg,dep,_) :: ra' ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (pat,names) = consume_pattern avoid Anonymous dep gl names in
let dest = get_recarg_dest dests in
safe_dest_intro_patterns avoid thin dest [pat] (fun ids thin ->
@@ -2415,7 +2415,7 @@ let induct_discharge dests avoid' tac (avoid,ra) names =
(* Marche pas... faut prendre en compte l'occurrence précise... *)
let atomize_param_of_ind (indref,nparams,_) hyp0 =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let reduce_to_quantified_ref = Tacmach.New.pf_apply reduce_to_quantified_ref gl in
let typ0 = reduce_to_quantified_ref indref tmptyp0 in
@@ -2424,7 +2424,7 @@ let atomize_param_of_ind (indref,nparams,_) hyp0 =
let params = List.firstn nparams argl in
(* le gl est important pour ne pas préévaluer *)
let rec atomize_one i avoid =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
if not (Int.equal i nparams) then
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
(* If argl <> [], we expect typ0 not to be quantified, in order to
@@ -2917,7 +2917,7 @@ let abstract_args gl generalize_vars dep id defined f args =
else None
let abstract_generalize ?(generalize_vars=true) ?(force_dep=false) id =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
Coqlib.check_required_library Coqlib.jmeq_module_name;
let (f, args, def, id, oldid) =
let oldid = Tacmach.New.pf_get_new_id id gl in
@@ -3359,7 +3359,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
induction applies with the induction hypotheses *)
let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names tac =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let (sigma, isrec, elim, indsign) = get_eliminator elim gl in
let names = compute_induction_names (Array.length indsign) names in
Tacticals.New.tclTHEN (Proofview.V82.tclEVARS sigma)
@@ -3374,7 +3374,7 @@ let apply_induction_with_discharge induct_tac elim indhyps destopt avoid names t
hypotheses from the context *)
let apply_induction_in_context hyp0 elim indvars names induct_tac =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let concl = Tacmach.New.pf_nf_concl gl in
let statuslists,lhyp0,indhyps,deps = cook_sign hyp0 indvars env in
@@ -3456,7 +3456,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
inhyps =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let tmptyp0 = Tacmach.New.pf_get_hyp_typ hyp0 gl in
let reduce_to_quantified_ref =
Tacmach.New.pf_apply reduce_to_quantified_ref gl
@@ -3474,7 +3474,7 @@ let induction_from_context clear_flag isrec with_evars (indref,nparams,elim) (hy
end
let induction_with_atomization_of_ind_arg clear_flag isrec with_evars elim names (hyp0,lbind) inhyps =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sigma, elim_info = find_induction_type isrec elim hyp0 gl in
Tacticals.New.tclTHENLIST
[Proofview.V82.tclEVARS sigma; (atomize_param_of_ind elim_info hyp0);
@@ -3486,7 +3486,7 @@ let induction_with_atomization_of_ind_arg clear_flag isrec with_evars elim names
scheme (which is mandatory for multiple ind args), check that all
parameters and arguments are given (mandatory too). *)
let induction_without_atomization isrec with_evars elim names lid =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let sigma, (indsign,scheme as elim_info) = find_elim_signature isrec elim (List.hd lid) gl in
let awaited_nargs =
scheme.nparams + scheme.nargs
@@ -3543,7 +3543,7 @@ let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbin
(induction_with_atomization_of_ind_arg
clear_flag isrec with_evars elim names (id,lbind) inhyps)
| _ ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let env = Proofview.Goal.env gl in
let x = id_of_name_using_hdchar (Global.env()) (typ_of env sigma c)
Anonymous in
@@ -3551,7 +3551,7 @@ let induction_gen clear_flag isrec with_evars elim (eqname,names) (sigma,(c,lbin
(* We need the equality name now *)
let with_eq = Option.map (fun eq -> (false,eq)) eqname in
(* TODO: if ind has predicate parameters, use JMeq instead of eq *)
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
Tacticals.New.tclTHEN
(* Warning: letin is buggy when c is not of inductive type *)
(letin_tac_gen with_eq
@@ -3584,7 +3584,7 @@ let induction_gen_l isrec with_evars elim (eqname,names) lc =
atomize_list l'
| _ ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let type_of = Tacmach.New.pf_type_of gl in
let x =
id_of_name_using_hdchar (Global.env()) (type_of c) Anonymous in
@@ -3615,7 +3615,7 @@ let induction_gen_l isrec with_evars elim (eqname,names) lc =
args *)
let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let ifi = is_functional_induction elim gl in
if Int.equal (List.length lc) 1 && not ifi then
(* standard induction *)
@@ -3706,7 +3706,7 @@ let simple_destruct = function
*)
let elim_scheme_type elim t =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let clause = Tacmach.New.of_old (fun gl -> mk_clenv_type_of gl elim) gl in
match kind_of_term (last_arg clause.templval.rebus) with
| Meta mv ->
@@ -3719,14 +3719,14 @@ let elim_scheme_type elim t =
end
let elim_type t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
let evd, elimc = find_ind_eliminator (fst ind) (Tacticals.New.elimination_sort_of_goal gl) gl in
Tacticals.New.tclTHEN (Proofview.V82.tclEVARS evd) (elim_scheme_type elimc t)
end
let case_type t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (ind,t) = Tacmach.New.pf_apply reduce_to_atomic_ind gl t in
let evd, elimc =
Tacmach.New.pf_apply build_case_analysis_scheme_default gl ind (Tacticals.New.elimination_sort_of_goal gl)
@@ -3752,7 +3752,7 @@ let maybe_betadeltaiota_concl allowred gl =
whd_betadeltaiota env sigma concl
let reflexivity_red allowred =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(* PL: usual reflexivity don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -3802,7 +3802,7 @@ let match_with_equation c =
Proofview.tclZERO NoEquationFound
let symmetry_red allowred =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(* PL: usual symmetry don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -3828,7 +3828,7 @@ let (forward_setoid_symmetry_in, setoid_symmetry_in) = Hook.make ()
let symmetry_in id =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let ctype = Tacmach.New.pf_type_of gl (mkVar id) in
let sign,t = decompose_prod_assum ctype in
Proofview.tclORELSE
@@ -3871,7 +3871,7 @@ let (forward_setoid_transitivity, setoid_transitivity) = Hook.make ()
(* This is probably not very useful any longer *)
let prove_transitivity hdcncl eq_kind t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let (eq1,eq2) = match eq_kind with
| MonomorphicLeibnizEq (c1,c2) ->
mkApp (hdcncl, [| c1; t|]), mkApp (hdcncl, [| t; c2 |])
@@ -3894,7 +3894,7 @@ let prove_transitivity hdcncl eq_kind t =
end
let transitivity_red allowred t =
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
(* PL: usual transitivity don't perform any reduction when searching
for an equality, but we may need to do some when called back from
inside setoid_reflexivity (see Optimize cases in setoid_replace.ml). *)
@@ -3940,7 +3940,7 @@ let abstract_subproof id gk tac =
let open Tacticals.New in
let open Tacmach.New in
let open Proofview.Notations in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let current_sign = Global.named_context()
and global_sign = Proofview.Goal.hyps gl in
let sign,secsign =
@@ -4061,7 +4061,7 @@ let admit_as_an_axiom =
(* >>>>>>> .merge_file_iUuzZK *)
let unify ?(state=full_transparent_state) x y =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
try
let flags =
{(default_unify_flags ()) with
@@ -4108,7 +4108,7 @@ module New = struct
open Locus
let refine c =
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let pf = Goal.refine_open_constr c in
Proofview.tclSENSITIVE pf <*>
Proofview.V82.tactic (reduce
diff --git a/toplevel/auto_ind_decl.ml b/toplevel/auto_ind_decl.ml
index 948a726b8..59306f9d4 100644
--- a/toplevel/auto_ind_decl.ml
+++ b/toplevel/auto_ind_decl.ml
@@ -357,7 +357,7 @@ let do_replace_lb lb_scheme_key aavoid narg p q =
)))
)
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let type_of_pq = Tacmach.New.of_old (fun gl -> pf_type_of gl p) gl in
let u,v = destruct_ind type_of_pq
in let lb_type_of_p =
@@ -418,7 +418,7 @@ let do_replace_bl bl_scheme_key (ind,u as indu) aavoid narg lft rgt =
let rec aux l1 l2 =
match (l1,l2) with
| (t1::q1,t2::q2) ->
- Proofview.Goal.raw_enter begin fun gl ->
+ Proofview.Goal.enter begin fun gl ->
let tt1 = Tacmach.New.pf_type_of gl t1 in
if eq_constr t1 t2 then aux q1 q2
else (
@@ -566,7 +566,7 @@ let compute_bl_tact bl_scheme_key ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end gl
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -589,7 +589,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Tacticals.New.tclREPEAT (
Tacticals.New.tclTHENLIST [
Simple.apply_in freshz (andb_prop());
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
(destruct false [None,Tacexpr.ElimOnConstr
(Evd.empty,((mkVar freshz,NoBindings)))]
@@ -603,7 +603,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
Ci a1 ... an = Ci b1 ... bn
replace bi with ai; auto || replace bi with ai by apply typeofbi_prod ; auto
*)
- Proofview.Goal.enter begin fun gls ->
+ Proofview.Goal.nf_enter begin fun gls ->
let gl = Proofview.Goal.concl gls in
match (kind_of_term gl) with
| App (c,ca) -> (
@@ -706,7 +706,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end gl
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -729,7 +729,7 @@ let compute_lb_tact lb_scheme_key ind lnamesparrec nparrec =
Tacticals.New.tclTHENLIST [apply (andb_true_intro());
simplest_split ;Auto.default_auto ]
);
- Proofview.Goal.enter begin fun gls ->
+ Proofview.Goal.nf_enter begin fun gls ->
let gl = Proofview.Goal.concl gls in
(* assume the goal to be eq (eq_type ...) = true *)
match (kind_of_term gl) with
@@ -852,7 +852,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
avoid := fresh::(!avoid); fresh
end gl
in
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let fresh_first_intros = List.map (fun id -> fresh_id id gl) first_intros in
let freshn = fresh_id (Id.of_string "x") gl in
let freshm = fresh_id (Id.of_string "y") gl in
@@ -885,7 +885,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
)
(Tacticals.New.tclTHEN (destruct_on eqbnm) Auto.default_auto);
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let freshH2 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENS (destruct_on_using (mkVar freshH) freshH2) [
(* left *)
@@ -897,7 +897,7 @@ let compute_dec_tact ind lnamesparrec nparrec =
;
(*right *)
- Proofview.Goal.enter begin fun gl ->
+ Proofview.Goal.nf_enter begin fun gl ->
let freshH3 = fresh_id (Id.of_string "H") gl in
Tacticals.New.tclTHENLIST [
simplest_right ;
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 13:06:58 +0000