From 771be16883c8c47828f278ce49545716918764c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>
Date: Sat, 12 Nov 2016 01:52:15 +0100
Subject: Hipattern API using EConstr.

---
 toplevel/indschemes.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'toplevel')

diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml
index 0723f16c3..9ed34d713 100644
--- a/toplevel/indschemes.ml
+++ b/toplevel/indschemes.ml
@@ -313,7 +313,7 @@ let warn_cannot_build_congruence =
           strbrk "Cannot build congruence scheme because eq is not found")
 
 let declare_congr_scheme ind =
-  if Hipattern.is_equality_type Evd.empty (mkInd ind) (** FIXME *) then begin
+  if Hipattern.is_equality_type Evd.empty (EConstr.of_constr (mkInd ind)) (** FIXME *) then begin
     if
       try Coqlib.check_required_library Coqlib.logic_module_name; true
       with e when CErrors.noncritical e -> false
-- 
cgit v1.2.3