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 /plugins/ltac/g_class.ml4 | |
| parent | a1fd5fb489237a1300adb242e2c9b6c74c82981b (diff) | |
Removing various tactic compatibility layers in core tactics.
Diffstat (limited to 'plugins/ltac/g_class.ml4')
| -rw-r--r-- | plugins/ltac/g_class.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4 index 40f30c794..ff5e7d5ff 100644 --- a/plugins/ltac/g_class.ml4 +++ b/plugins/ltac/g_class.ml4 @@ -85,7 +85,7 @@ TACTIC EXTEND not_evar END TACTIC EXTEND is_ground - [ "is_ground" constr(ty) ] -> [ Proofview.V82.tactic (is_ground ty) ] + [ "is_ground" constr(ty) ] -> [ is_ground ty ] END TACTIC EXTEND autoapply |