diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-11 12:34:07 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-25 15:13:25 -0400 |
| commit | b348a11ccc4913598b72e4ecbb58811bcccd7bfc (patch) | |
| tree | d28b04019de65139f7adf5300b68498dcc483b19 /tactics/tactics.mli | |
| 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/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
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 |