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

(limited to 'plugins/extraction/extraction.ml')

diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 2dca1d5e49..6869f9c47e 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -741,7 +741,7 @@ and extract_cst_app env sg mle mlt kn args =
   (* Can we instantiate types variables for this constant ? *)
   (* In Ocaml, inside the definition of this constant, the answer is no. *)
   let instantiated =
-    if lang () == Ocaml && List.mem_f Constant.equal kn !current_fixpoints
+    if lang () == Ocaml && List.mem_f Constant.CanOrd.equal kn !current_fixpoints
     then var2var' (snd schema)
     else instantiation schema
   in
-- 
cgit v1.2.3