diff options
| author | Jason Gross | 2017-04-11 12:34:07 -0400 |
|---|---|---|
| committer | Jason Gross | 2017-04-25 15:13:25 -0400 |
| commit | b348a11ccc4913598b72e4ecbb58811bcccd7bfc (patch) | |
| tree | d28b04019de65139f7adf5300b68498dcc483b19 /tactics | |
| parent | 12f34b2ebfcbe958ba53b49399c3fcaf01f7a18c (diff) | |
Make opaque optional only for tclABSTRACT
Also move named arguments to the beginning of the functions. As per
https://github.com/coq/coq/pull/201#discussion_r110928302
Diffstat (limited to 'tactics')
| -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 20de56645f..8f791cdcfe 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 082812c5a6..07a8035427 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 |