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.
---
 plugins/btauto/refl_btauto.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/btauto')

diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 23f8fe04a3..ac2058ba1b 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -115,7 +115,7 @@ module Bool = struct
     | Case (info, r, _iv, arg, pats) ->
       let is_bool =
         let i = info.ci_ind in
-        Names.eq_ind i (Lazy.force ind)
+        Names.Ind.CanOrd.equal i (Lazy.force ind)
       in
       if is_bool then
         Ifb ((aux arg), (aux pats.(0)), (aux pats.(1)))
-- 
cgit v1.2.3