From 2b91a8989687e152f7120aa6c907ffeba8495bab Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 22 Sep 2020 10:44:51 +0200
Subject: Deprecate the non-qualified equality functions on kerpairs.

This allows to quickly spot the parts of the code that rely on the canonical
ordering. When possible we directly introduce the quotient-aware versions.
---
 plugins/funind/invfun.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

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

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5d631aac84..118a917381 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -27,12 +27,13 @@ open Indfun_common
 *)
 let revert_graph kn post_tac hid =
   Proofview.Goal.enter (fun gl ->
+      let env = Proofview.Goal.env gl in
       let sigma = project gl in
       let typ = pf_get_hyp_typ hid gl in
       match EConstr.kind sigma typ with
       | App (i, args) when isInd sigma i ->
         let ((kn', num) as ind'), u = destInd sigma i in
-        if MutInd.equal kn kn' then
+        if Environ.QMutInd.equal env kn kn' then
           (* We have generated a graph hypothesis so that we must change it if we can *)
           let info =
             match find_Function_of_graph ind' with
-- 
cgit v1.2.3