aboutsummaryrefslogtreecommitdiff
path: root/interp/impargs.mli
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2019-04-02 13:22:11 +0200
committerEmilio Jesus Gallego Arias2019-05-10 01:57:54 +0200
commit1cdaa823aa2db2f68cf63561a85771bb98aec70f (patch)
tree4359c3c1051797f89202793e788ee145a0826521 /interp/impargs.mli
parent8ee7a4a7003fc2c5b01e0d6041961b3da14c0c84 (diff)
[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.
Diffstat (limited to 'interp/impargs.mli')
-rw-r--r--interp/impargs.mli4
1 files changed, 0 insertions, 4 deletions
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]. *)