From c6391a7edfd12a876f663bbac6d24386c021d148 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 19:49:37 +0200
Subject: Remove Evarutil.new_pure_evar_full from the API.

---
 engine/evarutil.mli | 2 --
 1 file changed, 2 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index b3c94e6b3b..c463415b6a 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -56,8 +56,6 @@ val new_pure_evar :
   ?principal:bool ->
   named_context_val -> evar_map -> types -> evar_map * Evar.t
 
-val new_pure_evar_full : evar_map -> ?typeclass_candidate:bool -> evar_info -> evar_map * Evar.t
-
 (** Create a new Type existential variable, as we keep track of
     them during type-checking and unification. *)
 val new_type_evar :
-- 
cgit v1.2.3


From aba870c6b58b18bc1bd4711c379863a87bbf6d33 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 19:54:19 +0200
Subject: Remove Evarutil.new_evar_from_context from the API.

---
 engine/evarutil.mli | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c463415b6a..c592a4f5d1 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -25,14 +25,6 @@ val mk_new_meta : unit -> constr
 
 (** {6 Creating a fresh evar given their type and context} *)
 
-val new_evar_from_context :
-  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?candidates:constr list ->
-  ?naming:intro_pattern_naming_expr ->
-  ?typeclass_candidate:bool ->
-  ?principal:bool ->
-  named_context_val -> evar_map  -> types -> evar_map * EConstr.t
-
 type naming_mode =
   | KeepUserNameAndRenameExistingButSectionNames
   | KeepUserNameAndRenameExistingEvenSectionNames
-- 
cgit v1.2.3


From 834c64015b608b8152e160d37e6f07a3106ff26b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 4 Jul 2020 20:02:42 +0200
Subject: Remove Evarutil.new_evar_instance from the API.

---
 engine/evarutil.mli | 15 ---------------
 1 file changed, 15 deletions(-)

(limited to 'engine/evarutil.mli')

diff --git a/engine/evarutil.mli b/engine/evarutil.mli
index c592a4f5d1..41b58d38b0 100644
--- a/engine/evarutil.mli
+++ b/engine/evarutil.mli
@@ -63,21 +63,6 @@ val new_Type : ?rigid:rigid -> evar_map -> evar_map * constr
 
 val new_global : evar_map -> GlobRef.t -> evar_map * constr
 
-(** Create a fresh evar in a context different from its definition context:
-   [new_evar_instance sign evd ty inst] creates a new evar of context
-   [sign] and type [ty], [inst] is a mapping of the evar context to
-   the context where the evar should occur. This means that the terms
-   of [inst] are typed in the occurrence context and their type (seen
-   as a telescope) is [sign] *)
-val new_evar_instance :
-  ?src:Evar_kinds.t Loc.located -> ?filter:Filter.t ->
-  ?abstract_arguments:Abstraction.t -> ?candidates:constr list ->
-  ?naming:intro_pattern_naming_expr ->
-  ?typeclass_candidate:bool ->
-  ?principal:bool ->
- named_context_val -> evar_map -> types ->
-  constr list -> evar_map * constr
-
 val make_pure_subst : evar_info -> 'a list -> (Id.t * 'a) list
 
 val safe_evar_value : evar_map -> Constr.existential -> Constr.constr option
-- 
cgit v1.2.3