diff options
| -rw-r--r-- | tactics/tactics.ml | 8 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
2 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 20de56645..8f791cdcf 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) ?(goal_type=None) tac tacK = +let cache_term_by_tactic_then ~opaque ?(goal_type=None) id gk tac tacK = let open Tacticals.New in let open Tacmach.New in let open Proofview.Notations in @@ -4985,8 +4985,8 @@ let cache_term_by_tactic_then id gk ?(opaque=true) ?(goal_type=None) tac tacK = Sigma.Unsafe.of_pair (tac, evd) end } -let abstract_subproof id gk tac ?(opaque=true) = - cache_term_by_tactic_then id gk ~opaque:opaque tac (fun lem args -> exact_no_check (applist (lem, args))) +let abstract_subproof ~opaque id gk tac = + cache_term_by_tactic_then ~opaque:opaque id gk tac (fun lem args -> exact_no_check (applist (lem, args))) let anon_id = Id.of_string "anonymous" @@ -5008,7 +5008,7 @@ let tclABSTRACT ?(opaque=true) name_op tac = let s, gk = if opaque then name_op_to_name name_op (Proof Theorem) "_subproof" else name_op_to_name name_op (DefinitionBody Definition) "_subterm" in - abstract_subproof s gk tac ~opaque:opaque + abstract_subproof ~opaque:opaque s gk tac let unify ?(state=full_transparent_state) x y = Proofview.Goal.s_enter { s_enter = begin fun gl -> diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 082812c5a..07a803542 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 -> ?goal_type:(constr option) -> unit Proofview.tactic -> (constr -> constr list -> unit Proofview.tactic) -> unit Proofview.tactic +val cache_term_by_tactic_then : opaque:bool -> ?goal_type:(constr option) -> Id.t -> Decl_kinds.goal_kind -> 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 |