1 files changed, 19 insertions, 8 deletions
diff --git a/engine/evarutil.ml b/engine/evarutil.ml
index 38ceed5690..1625f6fc81 100644
--- a/engine/evarutil.ml
+++ b/engine/evarutil.ml
@@ -13,7 +13,6 @@ open Util
 open Names
 open Term
 open Constr
-open Pre_env
 open Environ
 open Evd
 open Termops
@@ -437,12 +436,12 @@ let new_pure_evar_full evd evi =
   (evd, evk)
 
 let new_pure_evar?(src=default_source) ?(filter = Filter.identity) ?candidates ?(store = Store.empty) ?naming ?(principal=false) sign evd typ =
-  let default_naming = Misctypes.IntroAnonymous in
+  let default_naming = IntroAnonymous in
   let naming = Option.default default_naming naming in
   let name = match naming with
-  | Misctypes.IntroAnonymous -> None
-  | Misctypes.IntroIdentifier id -> Some id
-  | Misctypes.IntroFresh id ->
+  | IntroAnonymous -> None
+  | IntroIdentifier id -> Some id
+  | IntroFresh id ->
     let has_name id = try let _ = Evd.evar_key id evd in true with Not_found -> false in
     let id = Namegen.next_ident_away_from id has_name in
     Some id
@@ -515,6 +514,21 @@ let e_new_evar env evdref ?(src=default_source) ?filter ?candidates ?store ?nami
   evdref := evd';
   ev
 
+(* Safe interface to unification problems *)
+type unification_pb = conv_pb * env * EConstr.constr * EConstr.constr
+
+let eq_unification_pb evd (pbty,env,t1,t2) (pbty',env',t1',t2') =
+  pbty == pbty' && env == env' &&
+    EConstr.eq_constr evd t1 t1' &&
+    EConstr.eq_constr evd t2 t2'
+
+let add_unification_pb ?(tail=false) pb evd =
+  let conv_pbs = Evd.conv_pbs evd in
+  if not (List.exists (eq_unification_pb evd pb) conv_pbs) then
+    let (pbty,env,t1,t2) = pb in
+    Evd.add_conv_pb ~tail (pbty,env,t1,t2) evd
+  else evd
+
 (* This assumes an evar with identity instance and generalizes it over only
    the de Bruijn part of the context *)
 let generalize_evar_over_rels sigma (ev,args) =
@@ -876,6 +890,3 @@ let eq_constr_univs_test sigma1 sigma2 t u =
       (universes sigma2) fold t u sigma2
   in
   match ans with None -> false | Some _ -> true
-
-type type_constraint = EConstr.types option
-type val_constraint = EConstr.constr option