diff options
Diffstat (limited to 'plugins/ltac')
| -rw-r--r-- | plugins/ltac/tacexpr.ml | 35 | ||||
| -rw-r--r-- | plugins/ltac/tacexpr.mli | 35 | ||||
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 15 |
3 files changed, 11 insertions, 74 deletions
diff --git a/plugins/ltac/tacexpr.ml b/plugins/ltac/tacexpr.ml index 11d13d3a2f..8731cbf60d 100644 --- a/plugins/ltac/tacexpr.ml +++ b/plugins/ltac/tacexpr.ml @@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectNth of int - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectList of (int * int) list - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectId of Id.t - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectAll - [@ocaml.deprecated "Use constructors in [Goal_select]"] -[@@ocaml.deprecated "Use [Goal_select.t]"] - -type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = - | ElimOnConstr of 'a - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnIdent of lident - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnAnonHyp of int - [@ocaml.deprecated "Use constructors in [Tactics]"] -[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] - -type 'a destruction_arg = - clear_flag * 'a Tactics.core_destruction_arg -[@@ocaml.deprecated "Use Tactics.destruction_arg"] - -type inversion_kind = Inv.inversion_kind = - | SimpleInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversionClear - [@ocaml.deprecated "Use constructors in [Inv]"] -[@@ocaml.deprecated "Use Tactics.inversion_kind"] - type ('c,'d,'id) inversion_strength = | NonDepInversion of Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option diff --git a/plugins/ltac/tacexpr.mli b/plugins/ltac/tacexpr.mli index 6b131edaac..9958d6dcda 100644 --- a/plugins/ltac/tacexpr.mli +++ b/plugins/ltac/tacexpr.mli @@ -35,41 +35,6 @@ type advanced_flag = bool (* true = advanced false = basic *) type letin_flag = bool (* true = use local def false = use Leibniz *) type clear_flag = bool option (* true = clear hyp, false = keep hyp, None = use default *) -type goal_selector = Goal_select.t = - | SelectAlreadyFocused - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectNth of int - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectList of (int * int) list - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectId of Id.t - [@ocaml.deprecated "Use constructors in [Goal_select]"] - | SelectAll - [@ocaml.deprecated "Use constructors in [Goal_select]"] -[@@ocaml.deprecated "Use Vernacexpr.goal_selector"] - -type 'a core_destruction_arg = 'a Tactics.core_destruction_arg = - | ElimOnConstr of 'a - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnIdent of lident - [@ocaml.deprecated "Use constructors in [Tactics]"] - | ElimOnAnonHyp of int - [@ocaml.deprecated "Use constructors in [Tactics]"] -[@@ocaml.deprecated "Use Tactics.core_destruction_arg"] - -type 'a destruction_arg = - clear_flag * 'a Tactics.core_destruction_arg -[@@ocaml.deprecated "Use Tactics.destruction_arg"] - -type inversion_kind = Inv.inversion_kind = - | SimpleInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversion - [@ocaml.deprecated "Use constructors in [Inv]"] - | FullInversionClear - [@ocaml.deprecated "Use constructors in [Inv]"] -[@@ocaml.deprecated "Use Tactics.inversion_kind"] - type ('c,'d,'id) inversion_strength = | NonDepInversion of Inv.inversion_kind * 'id list * 'd or_and_intro_pattern_expr CAst.t or_var option diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 9f34df4608..f90e889678 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -283,6 +283,12 @@ let debugging_exception_step ist signal_anomaly e pp = debugging_step ist (fun () -> pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e) +let ensure_freshness env = + (* We anonymize declarations which we know will not be used *) + (* This assumes that the original context had no rels *) + process_rel_context + (fun d e -> EConstr.push_rel (Context.Rel.Declaration.set_name Anonymous d) e) env + (* Raise Not_found if not in interpretation sign *) let try_interp_ltac_var coerce ist env {loc;v=id} = let v = Id.Map.find id ist.lfun in @@ -1740,15 +1746,15 @@ and interp_atomic ist tac : unit Proofview.tactic = | AllOccurrences | NoOccurrences -> true | _ -> false in - let c_interp patvars sigma = + let c_interp patvars env sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in let ist = { ist with lfun = lfun' } in if is_onhyps && is_onconcl - then interp_type ist (pf_env gl) sigma c - else interp_constr ist (pf_env gl) sigma c + then interp_type ist env sigma c + else interp_constr ist env sigma c in Tactics.change None c_interp (interp_clause ist (pf_env gl) (project gl) cl) end @@ -1761,11 +1767,12 @@ and interp_atomic ist tac : unit Proofview.tactic = let sigma = project gl in let op = interp_typed_pattern ist env sigma op in let to_catch = function Not_found -> true | e -> CErrors.is_anomaly e in - let c_interp patvars sigma = + let c_interp patvars env sigma = let lfun' = Id.Map.fold (fun id c lfun -> Id.Map.add id (Value.of_constr c) lfun) patvars ist.lfun in + let env = ensure_freshness env in let ist = { ist with lfun = lfun' } in try interp_constr ist env sigma c |