From bc108fdf6cf42f3ce550f2f258adf7de5fa5bfdc Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Wed, 23 Sep 2020 12:42:21 +0200
Subject: Introduce an Ind module in the Names API.

This is similar to Constant and MutInd but for some reason this was was never
done. Such a patch makes the whole API more regular. We also deprecate the
legacy aliases.
---
 pretyping/pretyping.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'pretyping/pretyping.ml')

diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 268ad2ae56..06f7d92e62 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -813,7 +813,7 @@ struct
             try
               let IndType (indf, args) = find_rectype !!env sigma ty in
               let ((ind',u'),pars) = dest_ind_family indf in
-              if eq_ind ind ind' then List.map EConstr.of_constr pars
+              if Ind.CanOrd.equal ind ind' then List.map EConstr.of_constr pars
               else (* Let the usual code throw an error *) []
             with Not_found -> []
       else []
-- 
cgit v1.2.3