From c72bf7330bb32970616be4dddc7571f3b91c1562 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 01:08:53 +0100
Subject: Eqdecide API using EConstr.

---
 ltac/g_eqdecide.ml4 | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'ltac')

diff --git a/ltac/g_eqdecide.ml4 b/ltac/g_eqdecide.ml4
index 905653281c..6a49ea830b 100644
--- a/ltac/g_eqdecide.ml4
+++ b/ltac/g_eqdecide.ml4
@@ -23,5 +23,5 @@ TACTIC EXTEND decide_equality
 END
 
 TACTIC EXTEND compare
-| [ "compare" constr(c1) constr(c2) ] -> [ compare c1 c2 ]
+| [ "compare" constr(c1) constr(c2) ] -> [ compare (EConstr.of_constr c1) (EConstr.of_constr c2) ]
 END
-- 
cgit v1.2.3