diff options
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenvtac.ml | 4 | ||||
| -rw-r--r-- | proofs/proofview.ml | 24 | ||||
| -rw-r--r-- | proofs/proofview.mli | 12 | ||||
| -rw-r--r-- | proofs/tactic_debug.ml | 2 |
4 files changed, 21 insertions, 21 deletions
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml index 589cb5bdaa..d4826ce202 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 506d04f38a..48ca848915 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 b4a4a71970..72dcc8c375 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 62b157307a..19a1f77584 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 |