diff options
| author | Pierre-Marie Pédrot | 2016-11-19 02:45:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:28:59 +0100 |
| commit | 34e86e839be251717db96f1f5969d7724ab43097 (patch) | |
| tree | b62c2f97c7277250796b7f9b3783b95590ea98ab /ltac | |
| parent | 7b43de20a4acd7c9da290f038d9a16fe67eccd59 (diff) | |
Hints API using EConstr.
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 *) |