diff options
| -rw-r--r-- | tactics/tactics.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 6 insertions, 3 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 19627eb530..20de56645f 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4907,7 +4907,7 @@ let shrink_entry sign const = } in (const, args) -let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK = +let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -4927,7 +4927,10 @@ let cache_term_by_tactic_then id gk ?(opaque=true) tac tacK = else (Context.Named.add d s1,s2)) global_sign (Context.Named.empty, empty_named_context_val) in let id = next_global_ident_away id (pf_ids_of_hyps gl) in - let concl = it_mkNamedProd_or_LetIn (Proofview.Goal.concl gl) sign in + let concl = match goal_type with + | None -> Proofview.Goal.concl gl + | Some ty -> ty in + let concl = it_mkNamedProd_or_LetIn concl sign in let concl = try flush_and_check_evars !evdref concl with Uninstantiated_evar _ -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index d206011eed..082812c5a6 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -401,7 +401,7 @@ val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr - val unify : ?state:Names.transparent_state -> constr -> constr -> unit Proofview.tactic -val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic +val cache_term_by_tactic_then : Id.t -> Decl_kinds.goal_kind -> ?opaque:bool -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic val tclABSTRACT : ?opaque:bool -> Id.t option -> unit Proofview.tactic -> unit Proofview.tactic |