diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-07 16:19:24 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-05-08 20:44:29 +0200 |
| commit | e1e750683d52e7d2b63a707b62c4d2af0e01a532 (patch) | |
| tree | 4784d8750155dee00501bfa80765b2a7f8ffc8c0 /tactics/tactics.mli | |
| parent | 6522aa62d832837314dcef54735e6a4e55431571 (diff) | |
Isolating a function "make_abstraction", new name of "letin_abstract",
which compute an abstraction of the goal over a term or a pattern.
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 0ee307c23..b1d69a2a9 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -346,7 +346,7 @@ val forward : unit Proofview.tactic option -> intro_pattern_expr located optio val letin_tac : (bool * intro_pattern_expr located) option -> Name.t -> constr -> types option -> clause -> unit Proofview.tactic val letin_pat_tac : (bool * intro_pattern_expr located) option -> Name.t -> - evar_map * constr -> types option -> clause -> unit Proofview.tactic + evar_map * constr -> clause -> unit Proofview.tactic val assert_tac : Name.t -> types -> unit Proofview.tactic val assert_by : Name.t -> types -> unit Proofview.tactic -> unit Proofview.tactic val pose_proof : Name.t -> constr -> unit Proofview.tactic |