From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 pretyping/classops.ml | 1 +
 1 file changed, 1 insertion(+)

(limited to 'pretyping/classops.ml')

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index 9011186a3d..23d20dad3e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -51,6 +51,7 @@ type coe_info_typ = {
   coe_param : int }
 
 let coe_info_typ_equal c1 c2 =
+  let eq_constr c1 c2 = Termops.eq_constr Evd.empty (EConstr.of_constr c1) (EConstr.of_constr c2) in
   eq_constr c1.coe_value c2.coe_value &&
     eq_constr c1.coe_type c2.coe_type &&
     c1.coe_local == c2.coe_local &&
-- 
cgit v1.2.3