diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-16 20:37:15 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-24 17:59:21 +0200 |
| commit | 98da9fdce866728f93bc7cb690275f5559aa9bae (patch) | |
| tree | bc01065a1cca18ded5aa221e3c9e1a7c7ad316d8 /tactics/class_tactics.mli | |
| parent | a1fd5fb489237a1300adb242e2c9b6c74c82981b (diff) | |
Removing various tactic compatibility layers in core tactics.
Diffstat (limited to 'tactics/class_tactics.mli')
| -rw-r--r-- | tactics/class_tactics.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/class_tactics.mli b/tactics/class_tactics.mli index a38be5972..738cc0feb 100644 --- a/tactics/class_tactics.mli +++ b/tactics/class_tactics.mli @@ -33,7 +33,7 @@ val head_of_constr : Id.t -> constr -> unit Proofview.tactic val not_evar : constr -> unit Proofview.tactic -val is_ground : constr -> tactic +val is_ground : constr -> unit Proofview.tactic val autoapply : constr -> Hints.hint_db_name -> unit Proofview.tactic |