From 9f47342d890dc3ef7f4950004513a47d940af5ca Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Mon, 20 Nov 2017 03:09:43 +0100
Subject: [api] A few more minor deprecation notices.

Note the problem with `create_evar_defs`.
---
 engine/evarutil.mli  |  5 +++--
 engine/evd.mli       | 13 +++++++++----
 engine/universes.mli |  1 +
 3 files changed, 13 insertions(+), 6 deletions(-)

(limited to 'engine')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index 62288ced46..42f2d5f25a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -238,7 +238,8 @@ val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
 
 val meta_counter_summary_name : string
 
-(** Deprecater *)
-
+(** Deprecated *)
 type type_constraint = types option
+[@@ocaml.deprecated "use the version in Evardefine"]
 type val_constraint = constr option
+[@@ocaml.deprecated "use the version in Evardefine"]
diff --git a/engine/evd.mli b/engine/evd.mli
index af53735821..17fa150454 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -599,11 +599,16 @@ type open_constr = evar_map * constr (* Special case when before is empty *)
 type unsolvability_explanation = SeveralInstancesFound of int
 (** Failure explanation. *)
 
+(** {5 Summary names} *)
+
+(* This stuff is internal and should not be used. Currently a hack in
+   the STM relies on it. *)
+val evar_counter_summary_name : string
+
 (** {5 Deprecated functions} *)
+val create_evar_defs : evar_map -> evar_map
+(* XXX: This is supposed to be deprecated by used by ssrmatching, what
+   should the replacement be? *)
 
-val create_evar_defs      : evar_map -> evar_map
 (** Create an [evar_map] with empty meta map: *)
 
-(** {5 Summary names} *)
-
-val evar_counter_summary_name : string
diff --git a/engine/universes.mli b/engine/universes.mli
index 24613c4b91..a960099ed3 100644
--- a/engine/universes.mli
+++ b/engine/universes.mli
@@ -169,6 +169,7 @@ val constr_of_global : Globnames.global_reference -> constr
 
 (** ** DEPRECATED ** synonym of [constr_of_global] *)
 val constr_of_reference : Globnames.global_reference -> constr
+[@@ocaml.deprecated "synonym of [constr_of_global]"]
 
 (** Returns the type of the global reference, by creating a fresh instance of polymorphic 
     references and computing their instantiated universe context. (side-effect on the
-- 
cgit v1.2.3