Splitting Evarutil in two distinct files.

Some parts of Evarutils were related to the management of evars under constraints.
We put them in the Evardefine file.

11 files changed, 275 insertions, 225 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 8a55a7aaa5..c3968f8963 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -25,6 +25,7 @@ open Glob_ops
 open Retyping
 open Pretype_errors
 open Evarutil
+open Evardefine
 open Evarsolve
 open Evarconv
 open Evd
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 57b273d0d5..9d0f391e43 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -245,7 +245,7 @@ and coerce loc env evdref (x : Term.constr) (y : Term.constr)
 		       | Lambda (n, t, t') -> c, t'
 			   (*| Prod (n, t, t') -> t'*)
 		       | Evar (k, args) ->
-			   let (evs, t) = Evarutil.define_evar_as_lambda env !evdref (k,args) in
+			   let (evs, t) = Evardefine.define_evar_as_lambda env !evdref (k,args) in
 			     evdref := evs;
 			     let (n, dom, rng) = destLambda t in
 			     let dom = whd_evar !evdref dom in
@@ -375,7 +375,7 @@ let inh_app_fun_core env evd j =
     match kind_of_term t with
     | Prod (_,_,_) -> (evd,j)
     | Evar ev ->
-	let (evd',t) = define_evar_as_product evd ev in
+	let (evd',t) = Evardefine.define_evar_as_product evd ev in
 	  (evd',{ uj_val = j.uj_val; uj_type = t })
     | _ ->
       	try let t,p =
@@ -416,7 +416,7 @@ let inh_coerce_to_sort loc env evd j =
     match kind_of_term typ with
     | Sort s -> (evd,{ utj_val = j.uj_val; utj_type = s })
     | Evar ev when not (is_defined evd (fst ev)) ->
-	let (evd',s) = define_evar_as_sort env evd ev in
+	let (evd',s) = Evardefine.define_evar_as_sort env evd ev in
 	  (evd',{ utj_val = j.uj_val; utj_type = s })
     | _ ->
 	inh_tosort_force loc env evd j
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 489a8a729d..08973a05c4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -18,6 +18,7 @@ open Termops
 open Environ
 open Recordops
 open Evarutil
+open Evardefine
 open Evarsolve
 open Globnames
 open Evd
diff --git a/pretyping/evardefine.ml b/pretyping/evardefine.ml
new file mode 100644
index 0000000000..ef3a3f5255
--- /dev/null
+++ b/pretyping/evardefine.ml
@@ -0,0 +1,209 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Errors
+open Util
+open Pp
+open Names
+open Term
+open Vars
+open Termops
+open Namegen
+open Pre_env
+open Environ
+open Evd
+open Evarutil
+open Pretype_errors
+open Sigma.Notations
+
+let new_evar_unsafe env evd ?src ?filter ?candidates ?store ?naming ?principal typ =
+  let evd = Sigma.Unsafe.of_evar_map evd in
+  let Sigma (evk, evd, _) = new_evar env evd ?src ?filter ?candidates ?store ?naming ?principal typ in
+  (Sigma.to_evar_map evd, evk)
+
+let env_nf_evar sigma env =
+  let open Context.Rel.Declaration in
+  process_rel_context
+    (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env
+
+let env_nf_betaiotaevar sigma env =
+  let open Context.Rel.Declaration in
+  process_rel_context
+    (fun d e ->
+      push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env
+
+(****************************************)
+(* Operations on value/type constraints *)
+(****************************************)
+
+type type_constraint = types option
+
+type val_constraint = constr option
+
+(* Old comment...
+ * Basically, we have the following kind of constraints (in increasing
+ * strength order):
+ *   (false,(None,None)) -> no constraint at all
+ *   (true,(None,None))  -> we must build a judgement which _TYPE is a kind
+ *   (_,(None,Some ty))  -> we must build a judgement which _TYPE is ty
+ *   (_,(Some v,_))      -> we must build a judgement which _VAL is v
+ * Maybe a concrete datatype would be easier to understand.
+ * We differentiate (true,(None,None)) from (_,(None,Some Type))
+ * because otherwise Case(s) would be misled, as in
+ * (n:nat) Case n of bool [_]nat end  would infer the predicate Type instead
+ * of Set.
+ *)
+
+(* The empty type constraint *)
+let empty_tycon = None
+
+(* Builds a type constraint *)
+let mk_tycon ty = Some ty
+
+(* Constrains the value of a type *)
+let empty_valcon = None
+
+(* Builds a value constraint *)
+let mk_valcon c = Some c
+
+let idx = Namegen.default_dependent_ident
+
+(* Refining an evar to a product *)
+
+let define_pure_evar_as_product evd evk =
+  let open Context.Named.Declaration in
+  let evi = Evd.find_undefined evd evk in
+  let evenv = evar_env evi in
+  let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
+  let concl = Reductionops.whd_betadeltaiota evenv evd evi.evar_concl in
+  let s = destSort concl in
+  let evd1,(dom,u1) =
+    let evd = Sigma.Unsafe.of_evar_map evd in
+    let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
+    (Sigma.to_evar_map evd1, e)
+  in
+  let evd2,rng =
+    let newenv = push_named (LocalAssum (id, dom)) evenv in
+    let src = evar_source evk evd1 in
+    let filter = Filter.extend 1 (evar_filter evi) in
+      if is_prop_sort s then
+       (* Impredicative product, conclusion must fall in [Prop]. *)
+        new_evar_unsafe newenv evd1 concl ~src ~filter
+      else
+	let status = univ_flexible_alg in
+	let evd3, (rng, srng) =
+          let evd1 = Sigma.Unsafe.of_evar_map evd1 in
+          let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
+          (Sigma.to_evar_map evd3, e)
+        in
+	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
+	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
+	  evd3, rng
+  in
+  let prod = mkProd (Name id, dom, subst_var id rng) in
+  let evd3 = Evd.define evk prod evd2 in
+    evd3,prod
+
+(* Refine an applied evar to a product and returns its instantiation *)
+
+let define_evar_as_product evd (evk,args) =
+  let evd,prod = define_pure_evar_as_product evd evk in
+  (* Quick way to compute the instantiation of evk with args *)
+  let na,dom,rng = destProd prod in
+  let evdom = mkEvar (fst (destEvar dom), args) in
+  let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+  let evrng =  mkEvar (fst (destEvar rng), evrngargs) in
+  evd,mkProd (na, evdom, evrng)
+
+(* Refine an evar with an abstraction
+
+   I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where:
+   - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y)
+     or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B
+        with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type
+   - x1..xq,y:A |- ?e':B
+*)
+
+let define_pure_evar_as_lambda env evd evk =
+  let open Context.Named.Declaration in
+  let evi = Evd.find_undefined evd evk in
+  let evenv = evar_env evi in
+  let typ = Reductionops.whd_betadeltaiota evenv evd (evar_concl evi) in
+  let evd1,(na,dom,rng) = match kind_of_term typ with
+  | Prod (na,dom,rng) -> (evd,(na,dom,rng))
+  | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
+  | _ -> error_not_product_loc Loc.ghost env evd typ in
+  let avoid = ids_of_named_context (evar_context evi) in
+  let id =
+    next_name_away_with_default_using_types "x" na avoid (Reductionops.whd_evar evd dom) in
+  let newenv = push_named (LocalAssum (id, dom)) evenv in
+  let filter = Filter.extend 1 (evar_filter evi) in
+  let src = evar_source evk evd1 in
+  let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
+  let lam = mkLambda (Name id, dom, subst_var id body) in
+  Evd.define evk lam evd2, lam
+
+let define_evar_as_lambda env evd (evk,args) =
+  let evd,lam = define_pure_evar_as_lambda env evd evk in
+  (* Quick way to compute the instantiation of evk with args *)
+  let na,dom,body = destLambda lam in
+  let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
+  let evbody = mkEvar (fst (destEvar body), evbodyargs) in
+  evd,mkLambda (na, dom, evbody)
+
+let rec evar_absorb_arguments env evd (evk,args as ev) = function
+  | [] -> evd,ev
+  | a::l ->
+      (* TODO: optimize and avoid introducing intermediate evars *)
+      let evd,lam = define_pure_evar_as_lambda env evd evk in
+      let _,_,body = destLambda lam in
+      let evk = fst (destEvar body) in
+      evar_absorb_arguments env evd (evk, Array.cons a args) l
+
+(* Refining an evar to a sort *)
+
+let define_evar_as_sort env evd (ev,args) =
+  let evd, u = new_univ_variable univ_rigid evd in
+  let evi = Evd.find_undefined evd ev in 
+  let s = Type u in
+  let concl = Reductionops.whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
+  let sort = destSort concl in
+  let evd' = Evd.define ev (mkSort s) evd in
+  Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
+
+(* Propagation of constraints through application and abstraction:
+   Given a type constraint on a functional term, returns the type
+   constraint on its domain and codomain. If the input constraint is
+   an evar instantiate it with the product of 2 new evars. *)
+
+let split_tycon loc env evd tycon =
+  let rec real_split evd c =
+    let t = Reductionops.whd_betadeltaiota env evd c in
+      match kind_of_term t with
+	| Prod (na,dom,rng) -> evd, (na, dom, rng)
+	| Evar ev (* ev is undefined because of whd_betadeltaiota *) ->
+	    let (evd',prod) = define_evar_as_product evd ev in
+	    let (_,dom,rng) = destProd prod in
+	      evd',(Anonymous, dom, rng)
+	| App (c,args) when isEvar c ->
+	    let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
+	    real_split evd' (mkApp (lam,args))
+	| _ -> error_not_product_loc loc env evd c
+  in
+    match tycon with
+      | None -> evd,(Anonymous,None,None)
+      | Some c ->
+	  let evd', (n, dom, rng) = real_split evd c in
+	    evd', (n, mk_tycon dom, mk_tycon rng)
+
+let valcon_of_tycon x = x
+let lift_tycon n = Option.map (lift n)
+
+let pr_tycon env = function
+    None -> str "None"
+  | Some t -> Termops.print_constr_env env t
diff --git a/pretyping/evardefine.mli b/pretyping/evardefine.mli
new file mode 100644
index 0000000000..07b0e69d9f
--- /dev/null
+++ b/pretyping/evardefine.mli
@@ -0,0 +1,46 @@
+(************************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*   \VV/  **************************************************************)
+(*    //   *      This file is distributed under the terms of the       *)
+(*         *       GNU Lesser General Public License Version 2.1        *)
+(************************************************************************)
+
+open Names
+open Term
+open Evd
+open Environ
+
+val env_nf_evar : evar_map -> env -> env
+val env_nf_betaiotaevar : evar_map -> env -> env
+
+type type_constraint = types option
+type val_constraint = constr option
+
+val empty_tycon : type_constraint
+val mk_tycon : constr -> type_constraint
+val empty_valcon : val_constraint
+val mk_valcon : constr -> val_constraint
+
+(** Instantiate an evar by as many lambda's as needed so that its arguments
+    are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
+    [?y[vars1:=args1,vars:=args]] with
+    [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
+val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
+  evar_map * existential
+
+val split_tycon :
+  Loc.t -> env ->  evar_map -> type_constraint ->
+    evar_map * (Name.t * type_constraint * type_constraint)
+
+val valcon_of_tycon : type_constraint -> val_constraint
+val lift_tycon : int -> type_constraint -> type_constraint
+
+val define_evar_as_product : evar_map -> existential -> evar_map * types
+val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
+val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
+
+(** {6 debug pretty-printer:} *)
+
+val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
+
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index ab70de0578..35b66918cb 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -17,7 +17,6 @@ open Namegen
 open Pre_env
 open Environ
 open Evd
-open Reductionops
 open Pretype_errors
 open Sigma.Notations
 
@@ -76,17 +75,6 @@ let jv_nf_evar sigma = Array.map (j_nf_evar sigma)
 let tj_nf_evar sigma {utj_val=v;utj_type=t} =
   {utj_val=nf_evar sigma v;utj_type=t}
 
-let env_nf_evar sigma env =
-  let open Context.Rel.Declaration in
-  process_rel_context
-    (fun d e -> push_rel (map_constr (nf_evar sigma) d) e) env
-
-let env_nf_betaiotaevar sigma env =
-  let open Context.Rel.Declaration in
-  process_rel_context
-    (fun d e ->
-      push_rel (map_constr (Reductionops.nf_betaiota sigma) d) e) env
-
 let nf_evars_universes evm =
   Universes.nf_evars_and_universes_opt_subst (Reductionops.safe_evar_value evm) 
     (Evd.universe_subst evm)
@@ -481,7 +469,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
       | Evar (evk,l as ev) ->
 	  if Evd.is_defined !evdref evk then
 	    (* If evk is already defined we replace it by its definition *)
-	    let nc = whd_evar !evdref c in
+	    let nc = Reductionops.whd_evar !evdref c in
 	      (check_and_clear_in_constr env evdref err ids nc)
 	  else
 	    (* We check for dependencies to elements of ids in the
@@ -536,7 +524,7 @@ let rec check_and_clear_in_constr env evdref err ids c =
 	      let evi' = { evi with evar_extra = extra' } in
 	      evdref := Evd.add !evdref evk evi' ;
 	    (* spiwack: /hacking session *)
-              whd_evar !evdref c
+              Reductionops.whd_evar !evdref c
 
       | _ -> map_constr (check_and_clear_in_constr env evdref err ids) c
 
@@ -688,146 +676,6 @@ let occur_evar_upto sigma n c =
   in
   try occur_rec c; false with Occur -> true
 
-
-(****************************************)
-(* Operations on value/type constraints *)
-(****************************************)
-
-type type_constraint = types option
-
-type val_constraint = constr option
-
-(* Old comment...
- * Basically, we have the following kind of constraints (in increasing
- * strength order):
- *   (false,(None,None)) -> no constraint at all
- *   (true,(None,None))  -> we must build a judgement which _TYPE is a kind
- *   (_,(None,Some ty))  -> we must build a judgement which _TYPE is ty
- *   (_,(Some v,_))      -> we must build a judgement which _VAL is v
- * Maybe a concrete datatype would be easier to understand.
- * We differentiate (true,(None,None)) from (_,(None,Some Type))
- * because otherwise Case(s) would be misled, as in
- * (n:nat) Case n of bool [_]nat end  would infer the predicate Type instead
- * of Set.
- *)
-
-(* The empty type constraint *)
-let empty_tycon = None
-
-(* Builds a type constraint *)
-let mk_tycon ty = Some ty
-
-(* Constrains the value of a type *)
-let empty_valcon = None
-
-(* Builds a value constraint *)
-let mk_valcon c = Some c
-
-let idx = Namegen.default_dependent_ident
-
-(* Refining an evar to a product *)
-
-let define_pure_evar_as_product evd evk =
-  let open Context.Named.Declaration in
-  let evi = Evd.find_undefined evd evk in
-  let evenv = evar_env evi in
-  let id = next_ident_away idx (ids_of_named_context (evar_context evi)) in
-  let concl = whd_betadeltaiota evenv evd evi.evar_concl in
-  let s = destSort concl in
-  let evd1,(dom,u1) =
-    let evd = Sigma.Unsafe.of_evar_map evd in
-    let Sigma (e, evd1, _) = new_type_evar evenv evd univ_flexible_alg ~filter:(evar_filter evi) in
-    (Sigma.to_evar_map evd1, e)
-  in
-  let evd2,rng =
-    let newenv = push_named (LocalAssum (id, dom)) evenv in
-    let src = evar_source evk evd1 in
-    let filter = Filter.extend 1 (evar_filter evi) in
-      if is_prop_sort s then
-       (* Impredicative product, conclusion must fall in [Prop]. *)
-        new_evar_unsafe newenv evd1 concl ~src ~filter
-      else
-	let status = univ_flexible_alg in
-	let evd3, (rng, srng) =
-          let evd1 = Sigma.Unsafe.of_evar_map evd1 in
-          let Sigma (e, evd3, _) = new_type_evar newenv evd1 status ~src ~filter in
-          (Sigma.to_evar_map evd3, e)
-        in
-	let prods = Univ.sup (univ_of_sort u1) (univ_of_sort srng) in
-	let evd3 = Evd.set_leq_sort evenv evd3 (Type prods) s in
-	  evd3, rng
-  in
-  let prod = mkProd (Name id, dom, subst_var id rng) in
-  let evd3 = Evd.define evk prod evd2 in
-    evd3,prod
-
-(* Refine an applied evar to a product and returns its instantiation *)
-
-let define_evar_as_product evd (evk,args) =
-  let evd,prod = define_pure_evar_as_product evd evk in
-  (* Quick way to compute the instantiation of evk with args *)
-  let na,dom,rng = destProd prod in
-  let evdom = mkEvar (fst (destEvar dom), args) in
-  let evrngargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
-  let evrng =  mkEvar (fst (destEvar rng), evrngargs) in
-  evd,mkProd (na, evdom, evrng)
-
-(* Refine an evar with an abstraction
-
-   I.e., solve x1..xq |- ?e:T(x1..xq) with e:=λy:A.?e'[x1..xq,y] where:
-   - either T(x1..xq) = πy:A(x1..xq).B(x1..xq,y)
-     or T(x1..xq) = ?d[x1..xq] and we define ?d := πy:?A.?B
-        with x1..xq |- ?A:Type and x1..xq,y |- ?B:Type
-   - x1..xq,y:A |- ?e':B
-*)
-
-let define_pure_evar_as_lambda env evd evk =
-  let open Context.Named.Declaration in
-  let evi = Evd.find_undefined evd evk in
-  let evenv = evar_env evi in
-  let typ = whd_betadeltaiota evenv evd (evar_concl evi) in
-  let evd1,(na,dom,rng) = match kind_of_term typ with
-  | Prod (na,dom,rng) -> (evd,(na,dom,rng))
-  | Evar ev' -> let evd,typ = define_evar_as_product evd ev' in evd,destProd typ
-  | _ -> error_not_product_loc Loc.ghost env evd typ in
-  let avoid = ids_of_named_context (evar_context evi) in
-  let id =
-    next_name_away_with_default_using_types "x" na avoid (whd_evar evd dom) in
-  let newenv = push_named (LocalAssum (id, dom)) evenv in
-  let filter = Filter.extend 1 (evar_filter evi) in
-  let src = evar_source evk evd1 in
-  let evd2,body = new_evar_unsafe newenv evd1 ~src (subst1 (mkVar id) rng) ~filter in
-  let lam = mkLambda (Name id, dom, subst_var id body) in
-  Evd.define evk lam evd2, lam
-
-let define_evar_as_lambda env evd (evk,args) =
-  let evd,lam = define_pure_evar_as_lambda env evd evk in
-  (* Quick way to compute the instantiation of evk with args *)
-  let na,dom,body = destLambda lam in
-  let evbodyargs = Array.cons (mkRel 1) (Array.map (lift 1) args) in
-  let evbody = mkEvar (fst (destEvar body), evbodyargs) in
-  evd,mkLambda (na, dom, evbody)
-
-let rec evar_absorb_arguments env evd (evk,args as ev) = function
-  | [] -> evd,ev
-  | a::l ->
-      (* TODO: optimize and avoid introducing intermediate evars *)
-      let evd,lam = define_pure_evar_as_lambda env evd evk in
-      let _,_,body = destLambda lam in
-      let evk = fst (destEvar body) in
-      evar_absorb_arguments env evd (evk, Array.cons a args) l
-
-(* Refining an evar to a sort *)
-
-let define_evar_as_sort env evd (ev,args) =
-  let evd, u = new_univ_variable univ_rigid evd in
-  let evi = Evd.find_undefined evd ev in 
-  let s = Type u in
-  let concl = whd_betadeltaiota (evar_env evi) evd evi.evar_concl in
-  let sort = destSort concl in
-  let evd' = Evd.define ev (mkSort s) evd in
-  Evd.set_leq_sort env evd' (Type (Univ.super u)) sort, s
-
 (* We don't try to guess in which sort the type should be defined, since
    any type has type Type. May cause some trouble, but not so far... *)
 
@@ -835,38 +683,6 @@ let judge_of_new_Type evd =
   let Sigma (s, evd', p) = Sigma.new_univ_variable univ_rigid evd in
   Sigma ({ uj_val = mkSort (Type s); uj_type = mkSort (Type (Univ.super s)) }, evd', p)
 
-(* Propagation of constraints through application and abstraction:
-   Given a type constraint on a functional term, returns the type
-   constraint on its domain and codomain. If the input constraint is
-   an evar instantiate it with the product of 2 new evars. *)
-
-let split_tycon loc env evd tycon =
-  let rec real_split evd c =
-    let t = whd_betadeltaiota env evd c in
-      match kind_of_term t with
-	| Prod (na,dom,rng) -> evd, (na, dom, rng)
-	| Evar ev (* ev is undefined because of whd_betadeltaiota *) ->
-	    let (evd',prod) = define_evar_as_product evd ev in
-	    let (_,dom,rng) = destProd prod in
-	      evd',(Anonymous, dom, rng)
-	| App (c,args) when isEvar c ->
-	    let (evd',lam) = define_evar_as_lambda env evd (destEvar c) in
-	    real_split evd' (mkApp (lam,args))
-	| _ -> error_not_product_loc loc env evd c
-  in
-    match tycon with
-      | None -> evd,(Anonymous,None,None)
-      | Some c ->
-	  let evd', (n, dom, rng) = real_split evd c in
-	    evd', (n, mk_tycon dom, mk_tycon rng)
-
-let valcon_of_tycon x = x
-let lift_tycon n = Option.map (lift n)
-
-let pr_tycon env = function
-    None -> str "None"
-  | Some t -> Termops.print_constr_env env t
-
 let subterm_source evk (loc,k) =
   let evk = match k with
     | Evar_kinds.SubEvar (evk) -> evk
@@ -897,3 +713,6 @@ 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 = types option
+type val_constraint = constr option
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index bc4c37a918..a4f8527652 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -100,17 +100,6 @@ val is_ground_env  :  evar_map -> env -> bool
    new unresolved evar remains in [c] *)
 val check_evars : env -> evar_map -> evar_map -> constr -> unit
 
-val define_evar_as_product : evar_map -> existential -> evar_map * types
-val define_evar_as_lambda : env -> evar_map -> existential -> evar_map * types
-val define_evar_as_sort : env -> evar_map -> existential -> evar_map * sorts
-
-(** Instantiate an evar by as many lambda's as needed so that its arguments
-    are moved to the evar substitution (i.e. turn [?x[vars1:=args1] args] into
-    [?y[vars1:=args1,vars:=args]] with
-    [vars1 |- ?x:=\vars.?y[vars1:=vars1,vars:=vars]] *)
-val evar_absorb_arguments : env -> evar_map -> existential -> constr list ->
-  evar_map * existential
-
 (** [gather_dependent_evars evm seeds] classifies the evars in [evm]
     as dependent_evars and goals (these may overlap). A goal is an
     evar in [seeds] or an evar appearing in the (partial) definition
@@ -140,21 +129,6 @@ val occur_evar_upto : evar_map -> Evar.t -> Constr.t -> bool
 
 val judge_of_new_Type : 'r Sigma.t -> (unsafe_judgment, 'r) Sigma.sigma
 
-type type_constraint = types option
-type val_constraint = constr option
-
-val empty_tycon : type_constraint
-val mk_tycon : constr -> type_constraint
-val empty_valcon : val_constraint
-val mk_valcon : constr -> val_constraint
-
-val split_tycon :
-  Loc.t -> env ->  evar_map -> type_constraint ->
-    evar_map * (Name.t * type_constraint * type_constraint)
-
-val valcon_of_tycon : type_constraint -> val_constraint
-val lift_tycon : int -> type_constraint -> type_constraint
-
 (***********************************************************)
 
 (** [flush_and_check_evars] raise [Uninstantiated_evar] if an evar remains
@@ -177,9 +151,6 @@ val nf_evar_info : evar_map -> evar_info -> evar_info
 val nf_evar_map : evar_map -> evar_map
 val nf_evar_map_undefined : evar_map -> evar_map
 
-val env_nf_evar : evar_map -> env -> env
-val env_nf_betaiotaevar : evar_map -> env -> env
-
 val j_nf_betaiotaevar : evar_map -> unsafe_judgment -> unsafe_judgment
 val jv_nf_betaiotaevar :
   evar_map -> unsafe_judgment array -> unsafe_judgment array
@@ -212,11 +183,6 @@ val kind_of_term_upto : evar_map -> constr -> (constr,types) kind_of_term
     assumed to be an extention of those in [sigma1]. *)
 val eq_constr_univs_test : evar_map -> evar_map -> constr -> constr -> bool
 
-(** {6 debug pretty-printer:} *)
-
-val pr_tycon : env -> type_constraint -> Pp.std_ppcmds
-
-
 (** {6 Removing hyps in evars'context}
 raise OccurHypInSimpleClause if the removal breaks dependencies *)
 
@@ -251,3 +217,8 @@ val subterm_source : existential_key -> Evar_kinds.t Loc.located ->
   Evar_kinds.t Loc.located
 
 val meta_counter_summary_name : string
+
+(** Deprecater *)
+
+type type_constraint = types option
+type val_constraint = constr option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 8329de2ee4..30e26c6f89 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -36,6 +36,7 @@ open Typeops
 open Globnames
 open Nameops
 open Evarutil
+open Evardefine
 open Pretype_errors
 open Glob_term
 open Glob_ops
diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib
index b0d5a1df6a..e8c0bbbf90 100644
--- a/pretyping/pretyping.mllib
+++ b/pretyping/pretyping.mllib
@@ -9,6 +9,7 @@ Cbv
 Pretype_errors
 Find_subterm
 Evarutil
+Evardefine
 Evarsolve
 Recordops
 Evarconv
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 5347d965b5..52afa7f83a 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -39,7 +39,7 @@ let e_type_judgment env evdref j =
   match kind_of_term (whd_betadeltaiota env !evdref j.uj_type) with
     | Sort s -> {utj_val = j.uj_val; utj_type = s }
     | Evar ev ->
-        let (evd,s) = Evarutil.define_evar_as_sort env !evdref ev in
+        let (evd,s) = Evardefine.define_evar_as_sort env !evdref ev in
         evdref := evd; { utj_val = j.uj_val; utj_type = s }
     | _ -> error_not_type env j
 
@@ -61,7 +61,7 @@ let e_judge_of_apply env evdref funj argjv =
 	 else
 	   error_cant_apply_bad_type env (n,c1, hj.uj_type) funj argjv
       | Evar ev ->
-	  let (evd',t) = Evarutil.define_evar_as_product !evdref ev in
+	  let (evd',t) = Evardefine.define_evar_as_product !evdref ev in
           evdref := evd';
           let (_,_,c2) = destProd t in
 	  apply_rec (n+1) (subst1 hj.uj_val c2) restjl
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a7b415552a..a4a386530d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -19,6 +19,7 @@ open Evd
 open Reduction
 open Reductionops
 open Evarutil
+open Evardefine
 open Evarsolve
 open Pretype_errors
 open Retyping