diff options
| -rw-r--r-- | tactics/elim.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 20 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 |
4 files changed, 15 insertions, 15 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index d3aa16092..182240b55 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -161,8 +161,8 @@ let induction_trailer abs_i abs_j bargs = let double_ind h1 h2 = Proofview.Goal.nf_enter { 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_i = depth_of_quantified_hypothesis true h1 gl in + let abs_j = depth_of_quantified_hypothesis true h2 gl in let abs = if abs_i < abs_j then Proofview.tclUNIT (abs_i,abs_j) else if abs_i > abs_j then Proofview.tclUNIT (abs_j,abs_i) else diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 74ddd6b57..5f5adaafb 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1852,7 +1852,7 @@ and interp_atomic ist tac : unit Proofview.tactic = (* TODO: move sigma as a side-effect *) (* spiwack: the [*p] variants are for printing *) let cp = c in - let c = Tacmach.New.of_old (fun gl -> interp_induction_arg ist gl c) gl in + let c = interp_induction_arg ist gl c in let ipato = interp_intro_pattern_naming_option ist env sigma ipato in let ipatsp = ipats in let sigma,ipats = interp_or_and_intro_pattern_option ist env sigma ipats in diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 00afc99e8..c949a58b1 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -910,25 +910,25 @@ let intros_replacing ids = (* User-level introduction tactics *) -let pf_lookup_hypothesis_as_renamed env ccl = function +let lookup_hypothesis_as_renamed env ccl = function | AnonHyp n -> Detyping.lookup_index_as_renamed env ccl n | NamedHyp id -> Detyping.lookup_name_as_displayed env ccl id -let pf_lookup_hypothesis_as_renamed_gen red h gl = - let env = pf_env gl in +let lookup_hypothesis_as_renamed_gen red h gl = + let env = Proofview.Goal.env gl in let rec aux ccl = - match pf_lookup_hypothesis_as_renamed env ccl h with + match lookup_hypothesis_as_renamed env ccl h with | None when red -> aux (snd ((fst (Redexpr.reduction_of_red_expr env (Red true))) - env (project gl) ccl)) + env (Sigma.to_evar_map (Proofview.Goal.sigma gl)) ccl)) | x -> x in - try aux (Tacmach.pf_concl gl) + try aux (Proofview.Goal.concl gl) with Redelimination -> None -let is_quantified_hypothesis id g = - match pf_lookup_hypothesis_as_renamed_gen false (NamedHyp id) g with +let is_quantified_hypothesis id gl = + match lookup_hypothesis_as_renamed_gen false (NamedHyp id) gl with | Some _ -> true | None -> false @@ -940,7 +940,7 @@ let msg_quantified_hypothesis = function str " non dependent hypothesis" let depth_of_quantified_hypothesis red h gl = - match pf_lookup_hypothesis_as_renamed_gen red h gl with + match lookup_hypothesis_as_renamed_gen red h gl with | Some depth -> depth | None -> errorlabstrm "lookup_quantified_hypothesis" @@ -951,7 +951,7 @@ let depth_of_quantified_hypothesis red h gl = let intros_until_gen red h = Proofview.Goal.nf_enter { enter = begin fun gl -> - let n = Tacmach.New.of_old (depth_of_quantified_hypothesis red h) gl in + let n = depth_of_quantified_hypothesis red h gl in Tacticals.New.tclDO n (if red then introf else intro) end } diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2ae72f4a5..32483d050 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -25,7 +25,7 @@ open Locus (** {6 General functions. } *) -val is_quantified_hypothesis : Id.t -> goal sigma -> bool +val is_quantified_hypothesis : Id.t -> ([`NF],'b) Proofview.Goal.t -> bool (** {6 Primitive tactics. } *) @@ -73,7 +73,7 @@ val intros : unit Proofview.tactic (** [depth_of_quantified_hypothesis b h g] returns the index of [h] in the conclusion of goal [g], up to head-reduction if [b] is [true] *) val depth_of_quantified_hypothesis : - bool -> quantified_hypothesis -> goal sigma -> int + bool -> quantified_hypothesis -> ([`NF],'b) Proofview.Goal.t -> int val intros_until : quantified_hypothesis -> unit Proofview.tactic |