From 1cdaa823aa2db2f68cf63561a85771bb98aec70f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Tue, 2 Apr 2019 13:22:11 +0200
Subject: [api] Remove 8.10 deprecations.

Some of them are significant so presumably it will take a bit of
effort to fix overlays.

I left out the removal of `nf_enter` for now as MTac2 needs some
serious porting in order to avoid it.
---
 interp/impargs.ml  | 2 --
 interp/impargs.mli | 4 ----
 2 files changed, 6 deletions(-)

(limited to 'interp')

diff --git a/interp/impargs.ml b/interp/impargs.ml
index d83a0ce918..90fb5a2036 100644
--- a/interp/impargs.ml
+++ b/interp/impargs.ml
@@ -120,8 +120,6 @@ let argument_position_eq p1 p2 = match p1, p2 with
 | Hyp h1, Hyp h2 -> Int.equal h1 h2
 | _ -> false
 
-let explicitation_eq = Constrexpr_ops.explicitation_eq
-
 type implicit_explanation =
   | DepRigid of argument_position
   | DepFlex of argument_position
diff --git a/interp/impargs.mli b/interp/impargs.mli
index 0070423530..ccdd448460 100644
--- a/interp/impargs.mli
+++ b/interp/impargs.mli
@@ -143,7 +143,3 @@ val projection_implicits : env -> Projection.t -> implicit_status list ->
 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