Cleanup evar_extra: remove evar_info's store and add maps to evar_map

1 files changed, 19 insertions, 7 deletions

diff --git a/engine/evd.mli b/engine/evd.mli
index 1a5614988d..87f74f660d 100644
--- a/engine/evd.mli
+++ b/engine/evd.mli
@@ -83,10 +83,6 @@ type evar_body =
   | Evar_empty
   | Evar_defined of econstr
 
-
-module Store : Store.S
-(** Datatype used to store additional information in evar maps. *)
-
 type evar_info = {
   evar_concl : econstr;
   (** Type of the evar. *)
@@ -102,8 +98,6 @@ type evar_info = {
   (** Information about the evar. *)
   evar_candidates : econstr list option;
   (** List of possible solutions when known that it is a finite list *)
-  evar_extra : Store.t
-  (** Extra store, used for clever hacks. *)
 }
 
 val make_evar : named_context_val -> etypes -> evar_info
@@ -247,9 +241,24 @@ val restrict : Evar.t-> Filter.t -> ?candidates:econstr list ->
     possibly limiting the instances to a set of candidates (candidates
     are filtered according to the filter) *)
 
-val is_restricted_evar : evar_info -> Evar.t option
+val is_restricted_evar : evar_map -> Evar.t -> Evar.t option
 (** Tell if an evar comes from restriction of another evar, and if yes, which *)
 
+val set_resolvable_evar : evar_map -> Evar.t -> bool -> evar_map
+(** Declare an evar resolvable or unresolvable for typeclass resolution *)
+
+val unresolvable_evars : evar_map -> Evar.Set.t
+(** The set of unresolvable evars *)
+
+val is_resolvable_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared resolvable for typeclass resolution *)
+
+val set_obligation_evar : evar_map -> Evar.t -> evar_map
+(** Declare an evar as an obligation *)
+
+val is_obligation_evar : evar_map -> Evar.t -> bool
+(** Is the evar declared as an obligation *)
+
 val downcast : Evar.t-> etypes -> evar_map -> evar_map
 (** Change the type of an undefined evar to a new type assumed to be a
     subtype of its current type; subtyping must be ensured by caller *)
@@ -357,6 +366,9 @@ val add_universe_constraints : evar_map -> UnivProblem.Set.t -> evar_map
 
 *)
 
+module Store : Store.S
+(** Datatype used to store additional information in evar maps. *)
+
 val get_extra_data : evar_map -> Store.t
 val set_extra_data : Store.t -> evar_map -> evar_map