From 521a7b96c8963428ca0ecb39a22f458bf603ccab Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sat, 6 Sep 2014 17:09:51 +0200 Subject: 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. --- grammar/tacextend.ml4 | 2 +- plugins/btauto/refl_btauto.ml | 4 +- plugins/cc/cctac.ml | 14 ++--- plugins/fourier/fourierR.ml | 2 +- plugins/omega/coq_omega.ml | 14 ++--- plugins/quote/quote.ml | 4 +- plugins/setoid_ring/newring.ml4 | 4 +- proofs/clenvtac.ml | 4 +- proofs/proofview.ml | 24 ++++---- proofs/proofview.mli | 12 ++-- proofs/tactic_debug.ml | 2 +- tactics/auto.ml | 20 +++---- tactics/autorewrite.ml | 6 +- tactics/class_tactics.ml | 4 +- tactics/contradiction.ml | 10 ++-- tactics/elim.ml | 8 +-- tactics/eqdecide.ml | 10 ++-- tactics/equality.ml | 46 +++++++-------- tactics/evar_tactics.ml | 2 +- tactics/extratactics.ml4 | 18 +++--- tactics/ftactic.ml | 10 ++-- tactics/ftactic.mli | 4 +- tactics/inv.ml | 16 ++--- tactics/leminv.ml | 2 +- tactics/rewrite.ml | 10 ++-- tactics/tacinterp.ml | 88 +++++++++++++-------------- tactics/tacticals.ml | 28 ++++----- tactics/tactics.ml | 128 ++++++++++++++++++++-------------------- toplevel/auto_ind_decl.ml | 20 +++---- 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 "") 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 ; -- cgit v1.2.3