From 6d54c0fbbe8c905991dcb99112cce69792c9b142 Mon Sep 17 00:00:00 2001
From: Jasper Hugunin
Date: Sat, 16 Feb 2019 16:47:58 -0800
Subject: Deprecated duplicated explicitation_eq

---
 interp/impargs.ml  | 9 ++-------
 interp/impargs.mli | 1 +
 2 files changed, 3 insertions(+), 7 deletions(-)

(limited to 'interp')

diff --git a/interp/impargs.ml b/interp/impargs.ml
index 959455dfd2..841ce74538 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -120,12 +120,7 @@ let argument_position_eq p1 p2 = match p1, p2 with
 | Hyp h1, Hyp h2 -> Int.equal h1 h2
 | _ -> false
 
-let explicitation_eq ex1 ex2 = match ex1, ex2 with
-| ExplByPos (i1, id1), ExplByPos (i2, id2) ->
-  Int.equal i1 i2 && Option.equal Id.equal id1 id2
-| ExplByName id1, ExplByName id2 ->
-  Id.equal id1 id2
-| _ -> false
+let explicitation_eq = Constrexpr_ops.explicitation_eq
 
 type implicit_explanation =
   | DepRigid of argument_position
@@ -380,7 +375,7 @@ let flatten_explicitations l autoimps =
     | (Name id,_)::imps ->
        let value, l' =
          try
-           let eq = explicitation_eq in
+           let eq = Constrexpr_ops.explicitation_eq in
            let flags = List.assoc_f eq (ExplByName id) l in
            Some (Some id, flags), List.remove_assoc_f eq (ExplByName id) l
          with Not_found -> assoc_by_pos k l
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 4afc2af5e9..43c26b024f 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -138,4 +138,5 @@ val select_impargs_size : int -> implicits_list list -> implicit_status list
 val select_stronger_impargs : implicits_list list -> implicit_status list
 
 val explicitation_eq : Constrexpr.explicitation -> Constrexpr.explicitation -> bool
+  [@@ocaml.deprecated "Use Constrexpr_ops.explicitation_eq instead (since 8.10)"]
 (** Equality on [explicitation]. *)
-- 
cgit v1.2.3