diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 21:41:55 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2016-05-16 22:16:36 +0200 |
| commit | b3bfa1179bc6dda1a179e0ed5bc98dccdc1b3e14 (patch) | |
| tree | dd9e7016271fdad02452aed0f8cd469305e0780e /tactics/tactics.mli | |
| parent | a4bd166bd2119a5290276f0ded44f8186ba1ecee (diff) | |
Put the "generalize" tactic in the monad.
Diffstat (limited to 'tactics/tactics.mli')
| -rw-r--r-- | tactics/tactics.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f730dd6c4..9d02d3f6d 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -383,10 +383,9 @@ val letin_pat_tac : (bool * intro_pattern_naming) option -> (** {6 Generalize tactics. } *) -val generalize : constr list -> tactic -val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> tactic +val generalize : constr list -> unit Proofview.tactic +val generalize_gen : (constr Locus.with_occurrences * Name.t) list -> unit Proofview.tactic -val new_generalize : constr list -> unit Proofview.tactic val new_generalize_gen : ((occurrences * constr) * Name.t) list -> unit Proofview.tactic val generalize_dep : ?with_let:bool (** Don't lose let bindings *) -> constr -> tactic |