From aa3d78fefde6897a50273c83f944b6617963a9bc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 13:58:13 +0200
Subject: Similar introduction of a Construct module in the Names API.

---
 plugins/funind/glob_term_to_relation.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/glob_term_to_relation.ml')

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 6ed61043f9..767a9ec39b 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -332,7 +332,7 @@ let add_pat_variables sigma pat typ env : Environ.env =
       let constructors = Inductiveops.get_constructors env indf in
       let constructor : Inductiveops.constructor_summary =
         List.find
-          (fun cs -> eq_constructor c (fst cs.Inductiveops.cs_cstr))
+          (fun cs -> Construct.CanOrd.equal c (fst cs.Inductiveops.cs_cstr))
           (Array.to_list constructors)
       in
       let cs_args_types : types list =
@@ -402,7 +402,8 @@ let rec pattern_to_term_and_type env typ =
       let constructors = Inductiveops.get_constructors env indf in
       let constructor =
         List.find
-          (fun cs -> eq_constructor (fst cs.Inductiveops.cs_cstr) constr)
+          (fun cs ->
+            Construct.CanOrd.equal (fst cs.Inductiveops.cs_cstr) constr)
           (Array.to_list constructors)
       in
       let cs_args_types : types list =
-- 
cgit v1.2.3