diff options
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/g_auto.ml4 | 2 | ||||
| -rw-r--r-- | ltac/g_class.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4 index c6395d7e28..f540beb569 100644 --- a/ltac/g_auto.ml4 +++ b/ltac/g_auto.ml4 @@ -27,7 +27,7 @@ TACTIC EXTEND eassumption END TACTIC EXTEND eexact -| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact c ] +| [ "eexact" constr(c) ] -> [ Eauto.e_give_exact (EConstr.of_constr c) ] END let pr_hintbases _prc _prlc _prt = Pptactic.pr_hintbases diff --git a/ltac/g_class.ml4 b/ltac/g_class.ml4 index f8654d3903..ea9a2b6e17 100644 --- a/ltac/g_class.ml4 +++ b/ltac/g_class.ml4 @@ -74,7 +74,7 @@ TACTIC EXTEND is_ground END TACTIC EXTEND autoapply - [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply c i) ] + [ "autoapply" constr(c) "using" preident(i) ] -> [ Proofview.V82.tactic (autoapply (EConstr.of_constr c) i) ] END (** TODO: DEPRECATE *) |