diff options
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 40f30c7943..ff5e7d5ff2 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 |