portage modules Evarconv et Evarutil

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@161 85f007b7-540e-0410-9357-904b9bb8a0f7

14 files changed, 538 insertions, 470 deletions

diff --git a/.depend b/.depend
index 479d2d0e5f..0a04467eae 100644
--- a/.depend
+++ b/.depend
@@ -418,22 +418,24 @@ pretyping/coercion.cmx: pretyping/classops.cmx kernel/environ.cmx \
     pretyping/recordops.cmx kernel/reduction.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/coercion.cmi 
-pretyping/evarconv.cmo: pretyping/classops.cmi pretyping/evarutil.cmi \
-    kernel/generic.cmi kernel/names.cmi pretyping/recordops.cmi \
-    kernel/reduction.cmi kernel/term.cmi lib/util.cmi pretyping/evarconv.cmi 
-pretyping/evarconv.cmx: pretyping/classops.cmx pretyping/evarutil.cmx \
-    kernel/generic.cmx kernel/names.cmx pretyping/recordops.cmx \
-    kernel/reduction.cmx kernel/term.cmx lib/util.cmx pretyping/evarconv.cmi 
+pretyping/evarconv.cmo: pretyping/classops.cmi kernel/environ.cmi \
+    pretyping/evarutil.cmi kernel/generic.cmi kernel/instantiate.cmi \
+    kernel/names.cmi pretyping/recordops.cmi kernel/reduction.cmi \
+    kernel/term.cmi proofs/typing_ev.cmi lib/util.cmi pretyping/evarconv.cmi 
+pretyping/evarconv.cmx: pretyping/classops.cmx kernel/environ.cmx \
+    pretyping/evarutil.cmx kernel/generic.cmx kernel/instantiate.cmx \
+    kernel/names.cmx pretyping/recordops.cmx kernel/reduction.cmx \
+    kernel/term.cmx proofs/typing_ev.cmx lib/util.cmx pretyping/evarconv.cmi 
 pretyping/evarutil.cmo: kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    library/indrec.cmi kernel/names.cmi lib/pp.cmi kernel/reduction.cmi \
-    kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
-    pretyping/evarutil.cmi 
+    library/indrec.cmi kernel/instantiate.cmi kernel/names.cmi lib/pp.cmi \
+    pretyping/pretype_errors.cmi kernel/reduction.cmi kernel/sign.cmi \
+    kernel/term.cmi kernel/univ.cmi lib/util.cmi pretyping/evarutil.cmi 
 pretyping/evarutil.cmx: kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    library/indrec.cmx kernel/names.cmx lib/pp.cmx kernel/reduction.cmx \
-    kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
-    pretyping/evarutil.cmi 
-pretyping/pretype_errors.cmo: pretyping/pretype_errors.cmi 
-pretyping/pretype_errors.cmx: pretyping/pretype_errors.cmi 
+    library/indrec.cmx kernel/instantiate.cmx kernel/names.cmx lib/pp.cmx \
+    pretyping/pretype_errors.cmx kernel/reduction.cmx kernel/sign.cmx \
+    kernel/term.cmx kernel/univ.cmx lib/util.cmx pretyping/evarutil.cmi 
+pretyping/pretype_errors.cmo: kernel/names.cmi pretyping/pretype_errors.cmi 
+pretyping/pretype_errors.cmx: kernel/names.cmx pretyping/pretype_errors.cmi 
 pretyping/pretyping.cmo: parsing/ast.cmi pretyping/classops.cmi \
     pretyping/coercion.cmi kernel/environ.cmi pretyping/evarconv.cmi \
     pretyping/evarutil.cmi kernel/evd.cmi kernel/generic.cmi \
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 5f011c06d8..4bc551c6aa 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -933,7 +933,7 @@ let test_conversion f env sigma x y =
 
 let is_conv env sigma = test_conversion conv env sigma
 let is_conv_leq env sigma = test_conversion conv_leq env sigma
-
+let is_fconv = function | CONV -> is_conv | CONV_LEQ -> is_conv_leq
 
 (********************************************************************)
 (*             Special-Purpose Reduction                            *)
@@ -1268,30 +1268,30 @@ let poly_args env sigma t =
 
 exception Uninstantiated_evar of int
 
-let rec whd_ise env sigma = function
+let rec whd_ise sigma = function
   | DOPN(Evar sp,_) as k ->
       if Evd.in_dom sigma sp then
         if Evd.is_defined sigma sp then
-          whd_ise env sigma (existential_value sigma k)
+          whd_ise sigma (existential_value sigma k)
         else raise (Uninstantiated_evar sp)
       else k
-  | DOP2(Cast,c,_) -> whd_ise env sigma c
+  | DOP2(Cast,c,_) -> whd_ise sigma c
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
 
 
 (* 2- undefined existentials are left unchanged *)
-let rec whd_ise1 env sigma = function
+let rec whd_ise1 sigma = function
   | (DOPN(Evar sp,_) as k) ->
       if Evd.in_dom sigma sp & Evd.is_defined sigma sp then
-        whd_ise1 env sigma (existential_value sigma k)
+        whd_ise1 sigma (existential_value sigma k)
       else 
 	k
-  | DOP2(Cast,c,_) -> whd_ise1 env sigma c
+  | DOP2(Cast,c,_) -> whd_ise1 sigma c
   | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
   | c -> c
 
-let nf_ise1 env sigma = strong whd_ise1 env sigma
+let nf_ise1 sigma = strong (fun _ -> whd_ise1) empty_env sigma
 
 (* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
  * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 3e2fc9ffd1..9945b36cb7 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -172,6 +172,7 @@ val conv_forall2_i :
 
 val is_conv : unsafe_env -> 'a evar_map -> constr -> constr -> bool
 val is_conv_leq : unsafe_env -> 'a evar_map -> constr -> constr -> bool
+val is_fconv : conv_pb -> unsafe_env -> 'a evar_map -> constr -> constr -> bool
 
 
 (*s Special-Purpose Reduction Functions *)
@@ -182,11 +183,13 @@ val instance : (int * constr) list -> 'a reduction_function
 
 (* whd_ise raise Uninstantiated_evar if an evar remains uninstantiated *)
 (* the '*_ise1*' leave uninstantiated evar as it *)
+
 exception Uninstantiated_evar of int
-val whd_ise : 'a reduction_function
-val whd_ise1 : 'a reduction_function
-val nf_ise1 : 'a reduction_function
-val whd_ise1_metas : 'a reduction_function
+
+val whd_ise : 'a evar_map -> constr -> constr
+val whd_ise1 : 'a evar_map -> constr -> constr
+val nf_ise1 : 'a evar_map -> constr -> constr
+val whd_ise1_metas : 'a evar_map -> constr -> constr
 
 
 (*s Obsolete Reduction Functions *)
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index eaef2dafc0..f3cb78205a 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -29,6 +29,8 @@ type type_error =
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
   | CantFindCaseType of constr
+  | OccurCheck of int * constr
+  | NotClean of int * constr
 
 exception TypeError of path_kind * context * type_error
 
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index 23fed99f3e..a3820217ba 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -31,6 +31,8 @@ type type_error =
   | NotInductive of constr
   | MLCase of string * constr * constr * constr * constr
   | CantFindCaseType of constr
+  | OccurCheck of int * constr
+  | NotClean of int * constr
 
 exception TypeError of path_kind * context * type_error
 
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 83d38efa22..cd9e6d9211 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -6,6 +6,9 @@ open Names
 open Generic
 open Term
 open Reduction
+open Instantiate
+open Environ
+open Typing_ev
 open Classops
 open Recordops 
 open Evarutil
@@ -16,12 +19,12 @@ open Evarutil
  *)
 (* Fonctions temporaires pour relier la forme castée de la forme jugement *)
 let tjudge_of_cast_safe sigma env var =
-  match under_casts (nf_ise1 sigma) var with
-   DOP2 (Cast, b, t) ->
-     (match whd_betadeltaiota sigma t with
-	  DOP0 (Sort s) -> {body=b; typ=s}
-	| _ -> anomaly "Not a type (tjudge_of_cast)")
-  | c -> Mach.execute_rec_type sigma env c
+  match under_casts (fun _ -> nf_ise1) env sigma var with
+    | DOP2 (Cast, b, t) ->
+	(match whd_betadeltaiota env sigma t with
+	   | DOP0 (Sort s) -> {body=b; typ=s}
+	   | _ -> anomaly "Not a type (tjudge_of_cast)")
+    | c -> execute_rec_type env sigma c
 (* FIN TMP ***** *)
 
 
@@ -51,12 +54,12 @@ let tjudge_of_cast_safe sigma env var =
  * ass.
  *)
 
-let rec evar_apprec isevars stack c =
-  let (t,stack) = Reduction.apprec !isevars c stack in 
-  if ise_defined isevars t
-  then evar_apprec isevars stack (const_value !isevars t)
-  else (t,stack)
-
+let rec evar_apprec env isevars stack c =
+  let (t,stack) = Reduction.apprec env !isevars c stack in 
+  if ise_defined isevars t then 
+    evar_apprec env isevars stack (existential_value !isevars t)
+  else 
+    (t,stack)
 
 let conversion_problems = ref ([] : (conv_pb * constr * constr) list)
 
@@ -64,245 +67,268 @@ let reset_problems () = conversion_problems := []
 
 let add_conv_pb pb = (conversion_problems := pb::!conversion_problems)
 
-let get_changed_pb lsp =
-  let (pbs,pbs1) = List.fold_left
+let get_changed_pb lev =
+  let (pbs,pbs1) = 
+    List.fold_left
       (fun (pbs,pbs1) pb ->
-    	if status_changed lsp pb then (pb::pbs,pbs1)
-        else (pbs,pb::pbs1))
+    	 if status_changed lev pb then 
+	   (pb::pbs,pbs1)
+         else 
+	   (pbs,pb::pbs1))
       ([],[])
-      !conversion_problems in
+      !conversion_problems 
+  in
   conversion_problems := pbs1;
   pbs
 
-
-
 (* Precondition: one of the terms of the pb is an uninstanciated evar,
- * possibly applied to arguments.
- *)
-let rec solve_pb isevars pb =
-  match solve_simple_eqn (evar_conv_x isevars None CONV_X) isevars pb with
-    Some lsp ->
-      let pbs = get_changed_pb lsp in
-      List.for_all
- 	(fun (pbty,t1,t2) -> evar_conv_x isevars None pbty t1 t2)
- 	pbs
-  | None -> (add_conv_pb pb; true)
-
-and evar_conv_x isevars b pbty term1 term2 =
-  let term1 = whd_ise1 !isevars term1
-  and term2 = whd_ise1 !isevars term2 in
-   if eq_constr term1 term2 then true
-   else if (not(has_undefined_isevars isevars term1)) &
-            not(has_undefined_isevars isevars term2)
-   then fconv pbty !isevars term1 term2
-   else if ise_undefined isevars term1 or ise_undefined isevars term2
-   then solve_pb isevars (pbty,term1,term2)
-   else 
-     let (t1,l1) = evar_apprec isevars [] term1
-     and (t2,l2) = evar_apprec isevars [] term2 in
-     if (head_is_embedded_exist isevars t1 & not(is_eliminator t2))
-         or (head_is_embedded_exist isevars t2 & not(is_eliminator t1))
-     then (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true)
-     else evar_eqappr_x isevars b pbty (t1,l1) (t2,l2)
-
-and evar_eqappr_x isevars b pbty appr1 appr2 =
+ * possibly applied to arguments. *)
+
+let rec solve_pb env isevars pb =
+  match solve_simple_eqn (evar_conv_x env isevars CONV) isevars pb with
+    | Some lsp ->
+	let pbs = get_changed_pb lsp in
+	List.for_all
+ 	  (fun (pbty,t1,t2) -> evar_conv_x env isevars pbty t1 t2)
+ 	  pbs
+    | None -> (add_conv_pb pb; true)
+
+and evar_conv_x env isevars pbty term1 term2 =
+  let term1 = whd_ise1 !isevars term1 in
+  let term2 = whd_ise1 !isevars term2 in
+  if eq_constr term1 term2 then 
+    true
+  else if (not(has_undefined_isevars isevars term1)) &
+    not(has_undefined_isevars isevars term2) 
+  then 
+    is_fconv pbty env !isevars term1 term2
+  else if ise_undefined isevars term1 or ise_undefined isevars term2
+  then 
+    solve_pb env isevars (pbty,term1,term2)
+  else 
+    let (t1,l1) = evar_apprec env isevars [] term1 in
+    let (t2,l2) = evar_apprec env isevars [] term2 in
+    if (head_is_embedded_exist isevars t1 & not(is_eliminator t2))
+      or (head_is_embedded_exist isevars t2 & not(is_eliminator t1))
+    then 
+      (add_conv_pb (pbty,applist(t1,l1),applist(t2,l2)); true)
+    else 
+      evar_eqappr_x env isevars pbty (t1,l1) (t2,l2)
+	
+and evar_eqappr_x env isevars pbty appr1 appr2 =
   match (appr1,appr2) with
-    ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
-      let f1 () = 
-      	(ise_undefined isevars term1 or ise_undefined isevars term2) &
-	if List.length l1 > List.length l2 then 
-          let (deb1,rest1) = chop_list (List.length l1-List.length l2) l1
-          in solve_pb isevars(pbty,applist(term1,deb1),term2)
-            & for_all2eq (evar_conv_x isevars b CONV_X) rest1 l2
-	else
-	  let (deb2,rest2) = chop_list (List.length l2-List.length l1) l2
-          in solve_pb isevars(pbty,term1,applist(term2,deb2))
-            & for_all2eq (evar_conv_x isevars b CONV_X) l1 rest2
-      and f2 () =
-         (sp1 = sp2)
-       & (for_all2eq_vect (evar_conv_x isevars b CONV_X) al1 al2)  
-       & (for_all2eq (evar_conv_x isevars b CONV_X) l1 l2)
-      and f3 () =
-	 b<>None
-       & (try conv_record isevars b 
-           (try check_conv_record appr1 appr2
-           with Not_found -> check_conv_record appr2 appr1)
-          with _ -> false)
-      and f4 () =
-        if evaluable_const !isevars term2 then
-          evar_eqappr_x isevars b pbty
-            appr1 (evar_apprec isevars l2 (const_value !isevars term2))
-        else if evaluable_const !isevars term1 then
-          evar_eqappr_x isevars b pbty
-            (evar_apprec isevars l1 (const_value !isevars term1)) appr2
-        else false
-      in ise_try isevars [f1; f2; f3; f4]
-
-  | ((DOPN(Const _,_) as term1,l1),(t2,l2)) ->  
-      let f1 () =
-       	ise_undefined isevars term1 &
-       	(List.length l1 <= List.length l2) &
-       	let (deb2,rest2) = chop_list (List.length l2-List.length l1) l2
-        in solve_pb isevars(pbty,term1,applist(t2,deb2))
-          & for_all2eq (evar_conv_x isevars b CONV_X) l1 rest2
-      and f2 () =
-	b<>None &
- 	(try conv_record isevars b (check_conv_record appr1 appr2)
-        with _ -> false)
-      and f3 () = 
-	evaluable_const !isevars term1 &
- 	evar_eqappr_x isevars b pbty
-          (evar_apprec isevars l1 (const_value !isevars term1)) appr2
-      in ise_try isevars [f1; f2; f3]
-
-  | ((t1,l1),(DOPN(Const _,_) as t2,l2))  -> 
-      let f1 () =
-       	ise_undefined isevars t2 &
-       	(List.length l2 <= List.length l1) &
-       	let (deb1,rest1) = chop_list (List.length l1-List.length l2) l1
-        in solve_pb isevars(pbty,applist(t1,deb1),t2)
-          & for_all2eq (evar_conv_x isevars b CONV_X) rest1 l2
-      and f2 () = 
-	b<>None &
- 	(try (conv_record isevars b (check_conv_record appr2 appr1))
-        with _ -> false)
-      and f3 () =
-        evaluable_const !isevars t2 &
- 	evar_eqappr_x isevars b pbty
-          appr1 (evar_apprec isevars l2 (const_value !isevars t2))
-      in ise_try isevars [f1; f2; f3]
-
-  | ((DOPN(Abst _,_) as term1,l1),(DOPN(Abst _,_) as term2,l2)) ->
-      let f1 () =
-        (term1=term2) &
- 	(List.length(l1) = List.length(l2)) &
- 	(for_all2 (evar_conv_x isevars b CONV_X) l1 l2)
-      and f2 () =
-        if (evaluable_abst term2)
-	then evar_eqappr_x isevars b pbty
-               appr1 (evar_apprec isevars l2 (abst_value term2))
-	else evaluable_abst term1
-            & evar_eqappr_x isevars b pbty
-                (evar_apprec isevars l1 (abst_value term1)) appr2
-      in ise_try isevars [f1; f2]
-
-  | ((DOPN(Abst _,_) as term1,l1),_) ->  
-        (evaluable_abst term1)
-      & evar_eqappr_x isevars b pbty
-          (evar_apprec isevars l1 (abst_value term1)) appr2
-
-  | (_,(DOPN(Abst _,_) as term2,l2))  -> 
-        (evaluable_abst term2)
-      & evar_eqappr_x isevars b pbty
- 	  appr1 (evar_apprec isevars l2 (abst_value term2))
-
-  | ((Rel(n),l1),(Rel(m),l2)) ->
-	 n=m
-       & (List.length(l1) = List.length(l2))
-       & (for_all2 (evar_conv_x isevars b CONV_X) l1 l2)
-  | ((DOP2(Cast,c,_),l),_) -> evar_eqappr_x isevars b pbty (c,l) appr2
-  | (_,(DOP2(Cast,c,_),l)) -> evar_eqappr_x isevars b pbty appr1 (c,l)
-  | ((VAR id1,l1),(VAR id2,l2)) ->
-	 (id1=id2 & (List.length l1 = List.length l2)
-	    & (for_all2 (evar_conv_x isevars b CONV_X) l1 l2))
-  | ((DOP0(Meta(n)),l1),(DOP0(Meta(m)),l2)) ->
-	 (n=m & (List.length(l1) = List.length(l2))
-	    & (for_all2 (evar_conv_x isevars b CONV_X) l1 l2))
-  | ((DOP0(Sort s1),[]),(DOP0(Sort s2),[])) -> sort_cmp pbty s1 s2
-  | ((DOP2(Lambda,c1,DLAM(_,c2)),[]), (DOP2(Lambda,c'1,DLAM(_,c'2)),[])) -> 
-	  evar_conv_x isevars b CONV_X c1 c'1
-	    & evar_conv_x isevars b CONV_X c2 c'2
-  | ((DOP2(Prod,c1,DLAM(n,c2)),[]), (DOP2(Prod,c'1,DLAM(_,c'2)),[])) -> 
-         evar_conv_x isevars b CONV_X c1 c'1 
-         & evar_conv_x isevars
-	    (option_app
-	       (add_rel (n,tjudge_of_cast_safe !isevars (outSOME b) c1)) b)
-	    pbty c2 c'2
-  | ((DOPN(MutInd _ as o1,cl1) as ind1,l'1),
-     (DOPN(MutInd _ as o2,cl2) as ind2,l'2)) ->
-	  o1=o2
-	& for_all2eq_vect (evar_conv_x isevars b CONV_X) cl1 cl2
-        & for_all2eq (evar_conv_x isevars b CONV_X) l'1 l'2
-         
-  | ((DOPN(MutConstruct _ as o1,cl1) as constr1,l1),
-     (DOPN(MutConstruct _ as o2,cl2) as constr2,l2)) ->
-	  o1=o2
-        & for_all2eq_vect (evar_conv_x isevars b CONV_X) cl1 cl2
-        & for_all2eq (evar_conv_x isevars b CONV_X) l1 l2
-
-  | ((DOPN(MutCase _,_) as constr1,l'1),
-     (DOPN(MutCase _,_) as constr2,l'2)) ->
-	  let (_,p1,c1,cl1) = destCase constr1 in
-	  let (_,p2,c2,cl2) = destCase constr2 in
-	    evar_conv_x isevars b CONV_X p1 p2
-	  & evar_conv_x isevars b CONV_X c1 c2
-	  & (for_all2eq_vect (evar_conv_x isevars b CONV_X) cl1 cl2)
-	  & (for_all2eq (evar_conv_x isevars b CONV_X) l'1 l'2)
-
-  | ((DOPN(Fix _ as o1,cl1),l1),(DOPN(Fix _ as o2,cl2),l2))   ->
-	 o1=o2 & 
-	 (for_all2eq_vect (evar_conv_x isevars b CONV_X) cl1 cl2) &
-	 (for_all2eq (evar_conv_x isevars b CONV_X) l1 l2)
-
-  | ((DOPN(CoFix(i1),cl1),l1),(DOPN(CoFix(i2),cl2),l2))   ->
-	 i1=i2 & 
-	 (for_all2eq_vect (evar_conv_x isevars b CONV_X) cl1 cl2) &
-	 (for_all2eq (evar_conv_x isevars b CONV_X) l1 l2)
-
-  | (DOP0(Implicit),[]),(DOP0(Implicit),[]) -> true
-(* added to compare easily the specification of fixed points
- * But b (optional env) is not updated!
- *)
-  | (DLAM(_,c1),[]),(DLAM(_,c2),[]) -> evar_conv_x isevars b pbty c1 c2
-  | (DLAMV(_,vc1),[]),(DLAMV(_,vc2),[]) ->
-	 for_all2eq_vect (evar_conv_x isevars b pbty) vc1 vc2
-  | _ -> false
-
-
-and conv_record isevars ((Some env) as b) (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = 
-   let ks =
-     List.fold_left
-       (fun ks b ->
+    | ((DOPN(Const sp1,al1) as term1,l1), (DOPN(Const sp2,al2) as term2,l2)) ->
+	let f1 () = 
+      	  (ise_undefined isevars term1 or ise_undefined isevars term2) &
+	  if List.length l1 > List.length l2 then 
+            let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+            solve_pb env isevars(pbty,applist(term1,deb1),term2)
+            & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
+	  else
+	    let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+	    solve_pb env isevars(pbty,term1,applist(term2,deb2))
+            & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
+	and f2 () =
+          (sp1 = sp2)
+	  & (array_for_all2 (evar_conv_x env isevars CONV) al1 al2)  
+	  & (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+	and f3 () =
+	  (try conv_record env isevars 
+             (try check_conv_record appr1 appr2
+	      with Not_found -> check_conv_record appr2 appr1)
+           with _ -> false)
+	and f4 () =
+          if evaluable_constant env term2 then
+            evar_eqappr_x env isevars pbty
+              appr1 (evar_apprec env isevars l2 (constant_value env term2))
+          else if evaluable_constant env term1 then
+            evar_eqappr_x env isevars pbty
+              (evar_apprec env isevars l1 (constant_value env term1)) appr2
+          else 
+	    false
+	in 
+	ise_try isevars [f1; f2; f3; f4]
+
+    | ((DOPN(Const _,_) as term1,l1),(t2,l2)) ->  
+	let f1 () =
+       	  ise_undefined isevars term1 &
+       	  (List.length l1 <= List.length l2) &
+       	  let (deb2,rest2) = list_chop (List.length l2-List.length l1) l2 in
+	  solve_pb env isevars(pbty,term1,applist(t2,deb2))
+          & list_for_all2eq (evar_conv_x env isevars CONV) l1 rest2
+	and f2 () =
+	  (try conv_record env isevars (check_conv_record appr1 appr2)
+           with _ -> false)
+	and f3 () = 
+	  evaluable_constant env term1 &
+ 	  evar_eqappr_x env isevars pbty
+            (evar_apprec env isevars l1 (constant_value env term1)) appr2
+	in 
+	ise_try isevars [f1; f2; f3]
+	     
+    | ((t1,l1),(DOPN(Const _,_) as t2,l2))  -> 
+	let f1 () =
+       	  ise_undefined isevars t2 &
+       	  (List.length l2 <= List.length l1) &
+       	  let (deb1,rest1) = list_chop (List.length l1-List.length l2) l1 in
+	  solve_pb env isevars(pbty,applist(t1,deb1),t2)
+          & list_for_all2eq (evar_conv_x env isevars CONV) rest1 l2
+	and f2 () = 
+	  (try (conv_record env isevars (check_conv_record appr2 appr1))
+           with _ -> false)
+	and f3 () =
+          evaluable_constant env t2 &
+ 	  evar_eqappr_x env isevars pbty
+            appr1 (evar_apprec env isevars l2 (constant_value env t2))
+	in 
+	ise_try isevars [f1; f2; f3]
+
+    | ((DOPN(Abst _,_) as term1,l1),(DOPN(Abst _,_) as term2,l2)) ->
+	let f1 () =
+          (term1=term2) &
+ 	  (List.length(l1) = List.length(l2)) &
+ 	  (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
+	and f2 () =
+          if evaluable_abst env term2 then 
+	    evar_eqappr_x env isevars pbty
+              appr1 (evar_apprec env isevars l2 (abst_value env term2))
+	  else 
+	    evaluable_abst env term1
+            & evar_eqappr_x env isevars pbty
+              (evar_apprec env isevars l1 (abst_value env term1)) appr2
+	in 
+	ise_try isevars [f1; f2]
+
+    | ((DOPN(Abst _,_) as term1,l1),_) ->  
+        (evaluable_abst env term1)
+	& evar_eqappr_x env isevars pbty
+          (evar_apprec env isevars l1 (abst_value env term1)) appr2
+	  
+    | (_,(DOPN(Abst _,_) as term2,l2))  -> 
+        (evaluable_abst env term2)
+	& evar_eqappr_x env isevars pbty
+ 	  appr1 (evar_apprec env isevars l2 (abst_value env term2))
+
+    | ((Rel(n),l1),(Rel(m),l2)) ->
+	n=m
+	  & (List.length(l1) = List.length(l2))
+	  & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2)
+
+    | ((DOP2(Cast,c,_),l),_) -> evar_eqappr_x env isevars pbty (c,l) appr2
+
+    | (_,(DOP2(Cast,c,_),l)) -> evar_eqappr_x env isevars pbty appr1 (c,l)
+
+    | ((VAR id1,l1),(VAR id2,l2)) ->
+	(id1=id2 & (List.length l1 = List.length l2)
+	     & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2))
+
+    | ((DOP0(Meta(n)),l1),(DOP0(Meta(m)),l2)) ->
+	(n=m & (List.length(l1) = List.length(l2))
+	   & (List.for_all2 (evar_conv_x env isevars CONV) l1 l2))
+
+    | ((DOP0(Sort s1),[]),(DOP0(Sort s2),[])) -> base_sort_cmp pbty s1 s2
+
+    | ((DOP2(Lambda,c1,DLAM(_,c2)),[]), (DOP2(Lambda,c'1,DLAM(_,c'2)),[])) -> 
+	evar_conv_x env isevars CONV c1 c'1
+	& evar_conv_x env isevars CONV c2 c'2
+
+    | ((DOP2(Prod,c1,DLAM(n,c2)),[]), (DOP2(Prod,c'1,DLAM(_,c'2)),[])) -> 
+        evar_conv_x env isevars CONV c1 c'1 
+        & evar_conv_x 
+	  (push_rel (n,tjudge_of_cast_safe !isevars env c1) env) isevars
+	  pbty c2 c'2
+
+    | ((DOPN(MutInd _ as o1,cl1) as ind1,l'1),
+       (DOPN(MutInd _ as o2,cl2) as ind2,l'2)) ->
+	o1=o2
+	   & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
+           & list_for_all2eq (evar_conv_x env isevars CONV) l'1 l'2
+             
+    | ((DOPN(MutConstruct _ as o1,cl1) as constr1,l1),
+       (DOPN(MutConstruct _ as o2,cl2) as constr2,l2)) ->
+	o1=o2
+           & array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2
+           & list_for_all2eq (evar_conv_x env isevars CONV) l1 l2
+
+    | ((DOPN(MutCase _,_) as constr1,l'1),
+       (DOPN(MutCase _,_) as constr2,l'2)) ->
+	let (_,p1,c1,cl1) = destCase constr1 in
+	let (_,p2,c2,cl2) = destCase constr2 in
+	evar_conv_x env isevars CONV p1 p2
+	& evar_conv_x env isevars CONV c1 c2
+	& (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2)
+	& (list_for_all2eq (evar_conv_x env isevars CONV) l'1 l'2)
+
+    | ((DOPN(Fix _ as o1,cl1),l1),(DOPN(Fix _ as o2,cl2),l2))   ->
+	o1=o2 & 
+	   (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) &
+	   (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+	     
+    | ((DOPN(CoFix(i1),cl1),l1),(DOPN(CoFix(i2),cl2),l2))   ->
+	i1=i2 & 
+	   (array_for_all2 (evar_conv_x env isevars CONV) cl1 cl2) &
+	   (list_for_all2eq (evar_conv_x env isevars CONV) l1 l2)
+
+    (***
+    | (DOP0(Implicit),[]),(DOP0(Implicit),[]) -> true
+    (* added to compare easily the specification of fixed points
+     * But b (optional env) is not updated! *)
+    ***)
+
+    | (DLAM(_,c1),[]),(DLAM(_,c2),[]) -> 
+	evar_conv_x env isevars pbty c1 c2
+
+    | (DLAMV(_,vc1),[]),(DLAMV(_,vc2),[]) ->
+	array_for_all2 (evar_conv_x env isevars pbty) vc1 vc2
+
+    | _ -> false
+
+and conv_record env isevars (c,bs,(xs,xs1),(us,us1),(ts,ts1),t) = 
+  let ks =
+    List.fold_left
+      (fun ks b ->
 	 let (k,_) = new_isevar isevars env (substl ks b) CCI in (k::ks))
-       [] bs
-   in
-     if (for_all2eq 
-	   (fun u1 u -> evar_conv_x isevars b CONV_X u1 (substl ks u))
-	   us1 us)
-        &
-        (for_all2eq 
-	   (fun x1 x -> evar_conv_x isevars b CONV_X x1 (substl ks x))
-	   xs1 xs)
-        & (for_all2eq (evar_conv_x isevars b CONV_X) ts ts1)
-	& (evar_conv_x isevars b CONV_X t 
-	     (if ks=[] then c 
-	      else  (DOPN(AppL,Array.of_list(c::(List.rev ks))))))
-     then
- (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
-                          nbimplstruc:=!nbimplstruc+(List.length ks);true)
-                     else true)
-     else false
-
+      [] bs
+  in
+  if (list_for_all2eq 
+	(fun u1 u -> evar_conv_x env isevars CONV u1 (substl ks u))
+	us1 us)
+    &
+    (list_for_all2eq 
+       (fun x1 x -> evar_conv_x env isevars CONV x1 (substl ks x))
+       xs1 xs)
+    & (list_for_all2eq (evar_conv_x env isevars CONV) ts ts1)
+    & (evar_conv_x env isevars CONV t 
+	 (if ks=[] then c 
+	  else  (DOPN(AppL,Array.of_list(c::(List.rev ks))))))
+  then
+    (*TR*) (if !compter then (nbstruc:=!nbstruc+1;
+                              nbimplstruc:=!nbimplstruc+(List.length ks);true)
+            else true)
+  else false
 
 and check_conv_record (t1,l1) (t2,l2) = 
   try
     let {o_DEF=c;o_TABS=bs;o_TPARAMS=xs;o_TCOMPS=us} = 
       objdef_info (cte_of_constr t1,cte_of_constr t2) in
-    let xs1,t::ts = chop_list (List.length xs) l1 in
-    let us1,ts1= chop_list (List.length us) l2 in
+    let xs1,t,ts = 
+      match list_chop (List.length xs) l1 with 
+	| xs1,t::ts -> xs1,t,ts
+	| _ -> assert false 
+    in
+    let us1,ts1 = list_chop (List.length us) l2 in
     c,bs,(xs,xs1),(us,us1),(ts,ts1),t
-  with _ -> raise Not_found  (* try ... with _ -> ... *)
-
-
+  with _ -> 
+    raise Not_found
 
-let the_conv_x isevars env t1 t2 =
-  conv_x !isevars t1 t2 or evar_conv_x isevars (Some env) CONV_X t1 t2
+let the_conv_x env isevars t1 t2 =
+  is_conv env !isevars t1 t2 or evar_conv_x env isevars CONV t1 t2
 
 (* Si conv_x_leq repond true, pourquoi diable est-ce qu'on repasse une couche
  * avec evar_conv_x! Si quelqu'un comprend pourquoi, qu'il remplace ce
  * commentaire. Sinon, il va y avoir un bon coup de balai. B.B.
  *)
-let the_conv_x_leq isevars env t1 t2 =
-  conv_x_leq !isevars t1 t2
-  or evar_conv_x isevars (Some env) CONV_X_LEQ t1 t2     
+let the_conv_x_leq env isevars t1 t2 =
+  is_conv_leq env !isevars t1 t2
+  or evar_conv_x env isevars CONV_LEQ t1 t2     
  
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 0a44a9553e..59dfc7895c 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -10,13 +10,19 @@ open Evarutil
 (*i*)
 
 val reset_problems : unit -> unit
-val the_conv_x : unsafe_env -> 'a evar_defs -> constr -> constr -> bool
-val the_conv_x_leq : unsafe_env -> 'a evar_defs -> constr -> constr -> bool
 
+val the_conv_x : unsafe_env -> unit evar_defs -> constr -> constr -> bool
+
+val the_conv_x_leq : unsafe_env -> unit evar_defs -> constr -> constr -> bool
 
 (* For debugging *)
-val solve_pb : 'c evar_defs -> conv_pb * constr * constr -> bool
-val evar_conv_x : 'c evar_defs -> context option ->
-  conv_pb -> constr -> constr -> bool
-val evar_eqappr_x : 'c evar_defs -> context option ->
-  conv_pb -> constr * constr list -> constr * constr list -> bool
+val solve_pb : 
+  unsafe_env -> unit evar_defs -> conv_pb * constr * constr -> bool
+
+val evar_conv_x : 
+  unsafe_env -> unit evar_defs ->
+    conv_pb -> constr -> constr -> bool
+
+val evar_eqappr_x : 
+  unsafe_env -> unit evar_defs ->
+    conv_pb -> constr * constr list -> constr * constr list -> bool
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index f51bea7753..43653f80d4 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -10,8 +10,10 @@ open Term
 open Sign
 open Environ
 open Evd
+open Instantiate
 open Reduction
 open Indrec
+open Pretype_errors
 
 let rec filter_unique = function
   | [] -> []
@@ -51,7 +53,6 @@ let new_isevar_sign env sigma typ args =
 	       evar_body = Evar_empty; evar_info = () } in
   (Evd.add sigma newev info, mkEvar newev args)
 
-
 (* 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... *)
 let dummy_sort = mkType dummy_univ
@@ -89,30 +90,30 @@ let split_evar_to_arrow sigma c =
  * ?3 <-- ?1          no pb: env of ?3 is larger than ?1's
  * ?1 <-- (list ?2)   pb: ?2 may depend on x, but not ?1.
  * What we do is that ?2 is defined by a new evar ?4 whose context will be
- * a prefix of ?2's env, included in ?1's env.
- *)
+ * a prefix of ?2's env, included in ?1's env. *)
+
 let do_restrict_hyps sigma c =
-  let (ev,argsv) = destEvar c in
-  let args = Array.to_list argsv in
+  let (ev,args) = destEvar c in
+  let args = Array.to_list args in
   let evd = Evd.map sigma ev in
   let env = evd.evar_env in
+  let hyps = get_globals (context env) in
   let (_,(rsign,ncargs)) =
-    List.fold_left (fun (sign,(rs,na)) a ->
-      (tl_sign sign,
-       if not(closed0 a) then (rs,na)
-       else (add_sign (hd_sign sign) rs, a::na)))
-      (hyps,(nil_sign,[])) args in
-(*  let (_,(rsign,ncargs)) =
-    List.fold_left (fun (sign,(rs,na)) a ->
-      (tl_sign sign,
-       if not(closed0 a) then (nil_sign,[])
-       else (add_sign (hd_sign sign) rs, a::na)))
-      (hyps,(nil_sign,[])) args in *)
-  let nsign = rev_sign rsign in
-  let nargs = (Array.of_list (List.map mkVar (ids_of_sign nsign))) in
-  let (sigma',nc) = new_isevar_sign sigma nsign evd.concl nargs k in
-  let sigma'' = Evd.define sigma' sp nc in
-  (sigma'', mkConst (path_of_const nc) (Array.of_list (List.rev ncargs)))
+    List.fold_left 
+      (fun (sign,(rs,na)) a ->
+	 (tl_sign sign,
+	  if not(closed0 a) then 
+	    (rs,na)
+	  else 
+	    (add_sign (hd_sign sign) rs, a::na)))
+      (hyps,(nil_sign,[])) args 
+  in
+  let sign' = rev_sign rsign in
+  let env' = change_hyps (fun _ -> sign') env in
+  let args' = Array.of_list (List.map mkVar (ids_of_sign sign')) in
+  let (sigma',nc) = new_isevar_sign env' sigma evd.evar_concl args' in
+  let sigma'' = Evd.define sigma' ev nc in
+  (sigma'', nc)
 
 
 
@@ -149,48 +150,21 @@ let ise_map isevars sp = Evd.map !isevars sp
 let ise_define isevars sp body = isevars := Evd.define !isevars sp body
 
 (* Does k corresponds to an (un)defined existential ? *)
-let ise_undefined isevars k =
-  match k with
-    DOPN(Const _,_) ->
-      ise_in_dom isevars (path_of_const k) &
-      not (defined_const !isevars k)
+let ise_undefined isevars = function
+  | DOPN(Evar n,_) -> not (Evd.is_defined !isevars n)
   | _ -> false
 
-
-let ise_defined isevars k =
-  match k with
-    DOPN(Const _,_) -> Termenv.defined_existential !isevars k
+let ise_defined isevars = function
+  | DOPN(Evar n,_) -> Evd.is_defined !isevars n
   | _ -> false
 
-
 let restrict_hyps isevars c =
-  if ise_undefined isevars c & not (closed0 c)
-  then
-    (let (sigma,rc) = do_restrict_hyps !isevars c in
+  if ise_undefined isevars c & not (closed0 c) then begin
+    let (sigma,rc) = do_restrict_hyps !isevars c in
     isevars := sigma;
-    rc)
-  else c
-
-
-
-let error_occur_check sp rhs =
-  let id = string_of_id (Names.basename sp) in
-  let pt = prterm rhs in
-  errorlabstrm "Trad.occur_check"
-    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
-      'sTR" with term"; 'bRK(1,1); pt >]
-
-
-(* We need the environment here *)
-let error_not_clean sp t =
-  let c = Rel (List.hd (Listset.elements(free_rels t))) in
-  let id = string_of_id (Names.basename sp) in
-  let var = pTERM(c) in
-  errorlabstrm "Trad.not_clean"
-    [< 'sTR"Tried to define "; 'sTR id;
-       'sTR" with a term using variable "; var; 'sPC;
-       'sTR"which is not in its scope." >]
-
+    rc
+  end else 
+    c
 
 (* We try to instanciate the evar assuming the body won't depend
  * on arguments that are not Rels or VARs, or appearing several times.
@@ -215,30 +189,33 @@ let real_clean isevars sp args rhs =
     | DLAM(n,a) -> DLAM(n, subs (k+1) a)
     | DLAMV(n,v) -> DLAMV(n, Array.map (subs (k+1)) v) in
   let body = subs 0 rhs in
-  if not (closed0 body) then error_not_clean sp body;
+  if not (closed0 body) then error_not_clean CCI empty_env sp body;
   body
 
 
 
 (* [new_isevar] declares a new existential in an env env with type typ *)
 (* Converting the env into the sign of the evar to define *)
+
 let new_isevar isevars env typ k =
-  let (ENVIRON(sign,dbenv)) = env in
+  let (ENVIRON(sign,dbenv)) = context env in
   let t =
     List.fold_left (fun b (na,d)-> mkLambda na (incast_type d) b) typ dbenv in
   let rec aux sign = function
-      (0, t) -> (sign,t)
-    | (n, (DOP2(Lambda,d,(DLAM(na,b))))) ->
+    | (0, t) -> (sign,t)
+    | (n, DOP2(Lambda,d,(DLAM(na,b)))) ->
 	let na = if na = Anonymous then Name(id_of_string"_") else na in
        	let id = next_name_away na (ids_of_sign sign) in
        	aux (add_sign (id,(outcast_type d)) sign) (n-1, subst1 (VAR id) b)
-    | (_, _) -> anomaly "Trad.new_isevar" in
+    | (_, _) -> anomaly "Trad.new_isevar" 
+  in
   let (sign',typ') = aux sign (List.length dbenv, t) in
+  let env' = change_hyps (fun _ -> sign') env in
   let newargs =
     (List.rev(rel_list 0 (List.length dbenv)))
     @(List.map (fun id -> VAR id) (ids_of_sign sign)) in
   let (sigma',evar) =
-    new_isevar_sign !isevars sign' typ' (Array.of_list newargs) k in
+    new_isevar_sign env' !isevars typ' (Array.of_list newargs) in
   isevars := sigma';
   (evar,typ')
 
@@ -262,67 +239,76 @@ let new_isevar isevars env typ k =
  * ?1 would be instantiated by (le y y) but y is not in the scope of ?1
  *)
 let evar_define isevars lhs rhs =
-  let (sp,argsv) = destConst lhs in
-  let _ = if occur_opern (Const sp) rhs then error_occur_check sp rhs in
+  let (ev,argsv) = destEvar lhs in
+  if occur_opern (Evar ev) rhs then error_occur_check CCI empty_env ev rhs;
   let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
       (Array.to_list argsv) in 
-  let evd = ise_map isevars sp in
-  let hyps= evd.hyps in
+  let evd = ise_map isevars ev in
+  let hyps = get_globals (context evd.evar_env) in
   (* the substitution to invert *)
   let worklist = List.combine (ids_of_sign hyps) args in
-  let body = real_clean isevars sp worklist rhs in
-  ise_define isevars sp body;
-  [sp]
+  let body = real_clean isevars ev worklist rhs in
+  ise_define isevars ev body;
+  [ev]
 
 
 
 (* Solve pbs (?i x1..xn) = (?i y1..yn) which arises often in fixpoint
  * definitions. We try to unify the xi with the yi pairwise. The pairs
  * that don't unify are discarded (i.e. ?i is redefined so that it does not
- * depend on these args).
- *)
+ * depend on these args). *)
+
 let solve_refl conv_algo isevars c1 c2 =
-  let (sp,argsv1) = destConst c1
-  and (_,argsv2) = destConst c2 in
-  let evd = Evd.map !isevars sp in
-  let hyps = evd.Evd.hyps in
-  let (_,rsign) = it_vect2
+  let (ev,argsv1) = destEvar c1
+  and (_,argsv2) = destEvar c2 in
+  let evd = Evd.map !isevars ev in
+  let env = evd.evar_env in
+  let hyps = get_globals (context env) in
+  let (_,rsign) = 
+    array_fold_left2
       (fun (sgn,rsgn) a1 a2 ->
-	if conv_algo a1 a2
- 	then (tl_sign sgn, add_sign (hd_sign sgn) rsgn)
-	else (tl_sign sgn, rsgn))
-      (hyps,nil_sign) argsv1 argsv2 in
+	 if conv_algo a1 a2 then 
+	   (tl_sign sgn, add_sign (hd_sign sgn) rsgn)
+	 else 
+	   (tl_sign sgn, rsgn))
+      (hyps,nil_sign) argsv1 argsv2 
+  in
   let nsign = rev_sign rsign in
+  let nenv = change_hyps (fun _ -> nsign) env in
   let nargs = (Array.of_list (List.map mkVar (ids_of_sign nsign))) in
-  let newsp = new_isevar_path CCI in
+  let newev = Evd.new_evar () in
+  let info = { evar_concl = evd.evar_concl; evar_env = nenv;
+	       evar_body = Evar_empty; evar_info = () } in
   isevars :=
-    Evd.define (Evd.add_noinfo !isevars newsp nsign evd.Evd.concl)
-      sp (mkConst newsp nargs);
-  Some [sp]
+    Evd.define (Evd.add !isevars newev info) ev (mkEvar newev nargs);
+  Some [ev]
 
 
 (* Tries to solve problem t1 = t2.
  * Precondition: one of t1,t2 is an uninstanciated evar, possibly
  * applied to arguments.
  * Returns an optional list of evars that were instantiated, or None
- * if the problem couldn't be solved.
- *)
+ * if the problem couldn't be solved. *)
+
 (* Rq: uncomplete algorithm if pbty = CONV_X_LEQ ! *)
 let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) =
   let t1 = nf_ise1 !isevars t1 in
   let t2 = nf_ise1 !isevars t2 in
-  if eq_constr t1 t2 then Some []
-  else match (ise_undefined isevars t1, ise_undefined isevars t2) with
-    (true,true) ->
-      if path_of_const t1 = path_of_const t2
-      then solve_refl conv_algo isevars t1 t2
-      else if Array.length(args_of_const t1) < Array.length(args_of_const t2)
-      then Some (evar_define isevars t2 t1)
-      else Some (evar_define isevars t1 t2)
-  | (true,false) -> Some (evar_define isevars t1 t2)
-  | (false,true) -> Some (evar_define isevars t2 t1)
-  | _ -> None
-
+  if eq_constr t1 t2 then 
+    Some []
+  else 
+    match (ise_undefined isevars t1, ise_undefined isevars t2) with
+      | (true,true) ->
+	  if path_of_const t1 = path_of_const t2 then 
+	    solve_refl conv_algo isevars t1 t2
+	  else if Array.length(args_of_const t1) < 
+	          Array.length(args_of_const t2) then 
+	    Some (evar_define isevars t2 t1)
+	  else 
+	    Some (evar_define isevars t1 t2)
+      | (true,false) -> Some (evar_define isevars t1 t2)
+      | (false,true) -> Some (evar_define isevars t2 t1)
+      | _ -> None
 
 (*-------------------*)
 (* Now several auxiliary functions for the conversion algorithms modulo
@@ -332,69 +318,63 @@ let rec solve_simple_eqn conv_algo isevars ((pbty,t1,t2) as pb) =
 
 let has_undefined_isevars isevars c =
   let rec hasrec = function
-    DOPN(Const sp,cl) as k ->
-    if ise_in_dom isevars sp then 
-       if defined_const !isevars k
-       then hasrec (const_value !isevars k)
-       else failwith "caught"
-    else Array.iter hasrec cl
-
-  | DOP1(_,c) -> hasrec c
-  | DOP2(_,c1,c2) -> (hasrec c1; hasrec c2)
-  | DOPL(_,l) -> List.iter hasrec l
-  | DOPN(_,cl) -> Array.iter hasrec cl
-  | DLAM(_,c) -> hasrec c
-  | DLAMV(_,cl) -> Array.iter hasrec cl
-  | (VAR _|Rel _|DOP0 _) -> ()
- in (try (hasrec c ; false) with Failure "caught" -> true)
-    
-
+    | DOPN(Evar ev,cl) as k ->
+	if ise_in_dom isevars ev then 
+	  if ise_defined isevars k then 
+	    hasrec (existential_value !isevars k)
+	  else 
+	    failwith "caught"
+	else 
+	  Array.iter hasrec cl
+    | DOP1(_,c) -> hasrec c
+    | DOP2(_,c1,c2) -> (hasrec c1; hasrec c2)
+    | DOPL(_,l) -> List.iter hasrec l
+    | DOPN(_,cl) -> Array.iter hasrec cl
+    | DLAM(_,c) -> hasrec c
+    | DLAMV(_,cl) -> Array.iter hasrec cl
+    | (VAR _|Rel _|DOP0 _) -> ()
+  in 
+  (try (hasrec c ; false) with Failure "caught" -> true)
 
 let head_is_exist isevars = 
- let rec hrec = function
-    DOPN(Const _,_) as k -> ise_undefined isevars k
-  | DOPN(AppL,cl) -> hrec (hd_vect cl)
-  | DOP2(Cast,c,_) -> hrec c
-  | _ -> false
- in hrec 
-
-
+  let rec hrec = function
+    | DOPN(Evar _,_) as k -> ise_undefined isevars k
+    | DOPN(AppL,cl) -> hrec (array_hd cl)
+    | DOP2(Cast,c,_) -> hrec c
+    | _ -> false
+  in 
+  hrec 
 
 let rec is_eliminator = function
-    DOPN (AppL,_)          -> true
-  | DOPN(MutCase _,_) -> true
-  | DOP2 (Cast,c,_)        -> is_eliminator c
+  | DOPN (AppL,_)      -> true
+  | DOPN (MutCase _,_) -> true
+  | DOP2 (Cast,c,_)    -> is_eliminator c
   | _ -> false
 
-
 let head_is_embedded_exist isevars c =
-    (head_is_exist isevars c) & (is_eliminator c)
-
-
-let headconstant = 
- let rec hrec = function
-    DOPN(Const sp,_)       -> sp
-  | DOPN(MutCase _,_) as mc -> 
-       let (_,_,c,_) = destCase mc in
-       hrec c
-  | DOPN(AppL,cl)          -> hrec (hd_vect cl)
-  | DOP2(Cast,c,_)         -> hrec c
-  | _                      -> failwith "headconstant"
- in hrec 
-
-
-let status_changed lsp (pbty,t1,t2) =
-    try List.mem (headconstant t1) lsp or List.mem (headconstant t2) lsp
-    with Failure _ ->
-    try List.mem (headconstant t2) lsp
-    with Failure _ -> false
-
-
-
+  (head_is_exist isevars c) & (is_eliminator c)
+
+let head_evar = 
+  let rec hrec = function
+    | DOPN(Evar ev,_)       -> ev
+    | DOPN(MutCase _,_) as mc -> 
+	let (_,_,c,_) = destCase mc in hrec c
+    | DOPN(AppL,cl)          -> hrec (array_hd cl)
+    | DOP2(Cast,c,_)         -> hrec c
+    | _                      -> failwith "headconstant"
+  in 
+  hrec 
+    
+let status_changed lev (pbty,t1,t2) =
+  try 
+    List.mem (head_evar t1) lev or List.mem (head_evar t2) lev
+  with Failure _ ->
+    try List.mem (head_evar t2) lev with Failure _ -> false
 
 (* Operations on value/type constraints used in trad and progmach *)
 
 type trad_constraint = bool * (constr option * constr option)
+
 (* Basically, we have the following kind of constraints (in increasing
  * strength order):
  *   (false,(None,None)) -> no constraint at all
@@ -408,8 +388,6 @@ type trad_constraint = bool * (constr option * constr option)
  * of Set.
  *)
 
-
-
 (* The empty constraint *)
 let mt_tycon = (false,(None,None))
 
@@ -425,51 +403,49 @@ let mk_tycon2 (is_ass,_) ty = (is_ass,(None,Some ty))
 
 (* Given a type constraint on a term, returns the type constraint on its first
  * argument. If the input constraint is an evar instantiate it with the product
- * of 2 new evars.
- *)
-let prod_dom_tycon_unif isevars = function
-    None -> None
-  | Some c ->
-      (match whd_betadeltaiota !isevars c with
-        DOP2(Prod,c1,_) -> Some c1
-      |	t ->
-	  if (ise_undefined isevars t) then
-	    (let (sigma,dom,_) = split_evar_to_arrow !isevars t in
-	    isevars := sigma;
-	    Some dom)
-	  else None)
+ * of 2 new evars. *)
 
+let prod_dom_tycon_unif env isevars = function
+  | None -> None
+  | Some c ->
+      (match whd_betadeltaiota env !isevars c with
+         | DOP2(Prod,c1,_) -> Some c1
+	 | t ->
+	     if (ise_undefined isevars t) then begin
+	       let (sigma,dom,_) = split_evar_to_arrow !isevars t in
+	       isevars := sigma;
+	       Some dom
+	     end else 
+	       None)
 
 (* Given a constraint on a term, returns the constraint corresponding to its
- * first argument.
- *) 
-let app_dom_tycon isevars (_,(_,tyc)) =
-  (false,(None, prod_dom_tycon_unif isevars tyc))
+ * first argument. *) 
+
+let app_dom_tycon env isevars (_,(_,tyc)) =
+  (false,(None, prod_dom_tycon_unif env isevars tyc))
 
 
 (* Given a constraint on a term, returns the constraint corresponding to this
- * term applied to arg.
- *)
-let app_rng_tycon isevars arg = function
-    (_,(_,None)) as vtcon -> vtcon
-  | (_,(_,Some c)) ->
-      (match whd_betadeltaiota !isevars c with
-        DOP2(Prod,_,DLAM(_,b)) -> mk_tycon (subst1 arg b)
-      | _ -> mt_tycon)
+ * term applied to arg. *)
 
+let app_rng_tycon env isevars arg = function
+  | (_,(_,None)) as vtcon -> vtcon
+  | (_,(_,Some c)) ->
+      (match whd_betadeltaiota env !isevars c with
+         | DOP2(Prod,_,DLAM(_,b)) -> mk_tycon (subst1 arg b)
+	 | _ -> mt_tycon)
 
 (* Given a constraint on an abstraction, returns the constraint on the value
  * of the domain type. If we had no constraint, we still know it should be
- * a type.
- *)
-let abs_dom_valcon isevars (_,(_,tyc)) =
-  (true,(prod_dom_tycon_unif isevars tyc, None))
-
+ * a type. *)
+      
+let abs_dom_valcon env isevars (_,(_,tyc)) =
+  (true,(prod_dom_tycon_unif env isevars tyc, None))
 
 (* Given a constraint on an abstraction, returns the constraint on the body *)
-let abs_rng_tycon isevars = function
-    (_,(_,None)) -> mt_tycon
+let abs_rng_tycon env isevars = function
+  | (_,(_,None)) -> mt_tycon
   | (_,(_,Some c)) ->
-      (match whd_betadeltaiota !isevars c with
-      | DOP2(Prod,_,DLAM(_,b)) -> mk_tycon b
-      | _ -> mt_tycon)
+      (match whd_betadeltaiota env !isevars c with
+	 | DOP2(Prod,_,DLAM(_,b)) -> mk_tycon b
+	 | _ -> mt_tycon)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index d7ef3620fb..c8d6b91acc 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -19,7 +19,7 @@ val filter_sign :
   'a * identifier list * var_context
 
 val dummy_sort : constr
-val do_restrict_hyps : 'a evar_map -> constr -> 'a evar_map * constr
+val do_restrict_hyps : unit evar_map -> constr -> unit evar_map * constr
 
 
 type 'a evar_defs = 'a evar_map ref
@@ -30,20 +30,19 @@ val ise_undefined : 'a evar_defs -> constr -> bool
 val ise_defined : 'a evar_defs -> constr -> bool
 
 val real_clean :
-  'a evar_defs ->
-  section_path -> (identifier * constr) list -> constr -> constr
+  unit evar_defs -> int -> (identifier * constr) list -> constr -> constr
 val new_isevar :
-  unsafe_env -> 'a evar_defs -> constr -> path_kind -> constr * constr
-val evar_define : 'a evar_defs -> constr -> constr -> section_path list
-val solve_simple_eqn : (constr -> constr -> bool) -> 'a evar_defs ->
-  (conv_pb * constr * constr) -> section_path list option
+  unit evar_defs -> unsafe_env -> constr -> path_kind -> constr * constr
+val evar_define : unit evar_defs -> constr -> constr -> int list
+val solve_simple_eqn : (constr -> constr -> bool) -> unit evar_defs ->
+  (conv_pb * constr * constr) -> int list option
 
 val has_undefined_isevars : 'a evar_defs -> constr -> bool
 val head_is_exist : 'a evar_defs -> constr -> bool
 val is_eliminator : constr -> bool
 val head_is_embedded_exist : 'a evar_defs -> constr -> bool
-val headconstant : constr -> section_path
-val status_changed : section_path list -> conv_pb * constr * constr -> bool
+val head_evar : constr -> int
+val status_changed : int list -> conv_pb * constr * constr -> bool
 
 
 (* Value/Type constraints *)
@@ -56,13 +55,16 @@ val mk_tycon : constr -> trad_constraint
 val mk_tycon2 : trad_constraint -> constr -> trad_constraint
 
 (* application *)
-val app_dom_tycon : 'a evar_defs -> trad_constraint -> trad_constraint
+val app_dom_tycon : 
+  unsafe_env -> unit evar_defs -> trad_constraint -> trad_constraint
 val app_rng_tycon :
-  'a evar_defs -> constr -> trad_constraint -> trad_constraint
+  unsafe_env -> 'a evar_defs -> constr -> trad_constraint -> trad_constraint
 
 (* abstraction *)
-val abs_dom_valcon : 'a evar_defs -> trad_constraint -> trad_constraint
-val abs_rng_tycon : 'a evar_defs -> trad_constraint -> trad_constraint
+val abs_dom_valcon : 
+  unsafe_env -> unit evar_defs -> trad_constraint -> trad_constraint
+val abs_rng_tycon : 
+  unsafe_env -> 'a evar_defs -> trad_constraint -> trad_constraint
 
 
 (* $Id$ *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
index 8892eaf7fa..c3baf8ea06 100644
--- a/pretyping/pretype_errors.ml
+++ b/pretyping/pretype_errors.ml
@@ -1,4 +1,14 @@
 
+(* $Id$ *)
+
+open Names
+open Sign
+open Environ
+open Type_errors
+open Rawterm
+
+exception PretypeError of loc * path_kind * context * type_error
+
 let error_cant_find_case_type_loc loc env expr =
   raise (PretypeError (loc,CCI,context env,CantFindCaseType expr))
 
@@ -7,3 +17,13 @@ let error_ill_formed_branch k env c i actty expty =
 
 let error_number_branches_loc loc k env c ct expn =
   raise (PretypeError (loc, k, context env, NumberBranches (c,ct,expn)))
+
+let error_ill_formed_branch_loc loc k env c i actty expty =
+  raise (PretypeError (loc, k, context env, IllFormedBranch (c,i,actty,expty)))
+
+let error_occur_check k env ev c =
+  raise (TypeError (k, context env, OccurCheck (ev,c)))
+
+let error_not_clean k env ev c =
+  raise (TypeError (k, context env, NotClean (ev,c)))
+
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
index c8f6dc463b..ac605f196a 100644
--- a/pretyping/pretype_errors.mli
+++ b/pretyping/pretype_errors.mli
@@ -11,9 +11,10 @@ open Rawterm
 
 (* The type of errors raised by the pretyper *)
 
-exception PreTypeError of loc * path_kind * context * type_error
+exception PretypeError of loc * path_kind * context * type_error
 
-val error_cant_find_case_type_loc : loc -> unsafe_env -> constr -> 'a
+val error_cant_find_case_type_loc : 
+  loc -> unsafe_env -> constr -> 'a
 
 val error_ill_formed_branch_loc : 
   loc -> path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b
@@ -21,3 +22,8 @@ val error_ill_formed_branch_loc :
 val error_number_branches_loc : 
   loc -> path_kind -> unsafe_env -> constr -> constr -> int -> 'b
 
+val error_occur_check : path_kind -> unsafe_env -> int -> constr -> 'a
+
+val error_not_clean : path_kind -> unsafe_env -> int -> constr -> 'a
+
+
diff --git a/proofs/typing_ev.ml b/proofs/typing_ev.ml
index 5e48153719..741ef10409 100644
--- a/proofs/typing_ev.ml
+++ b/proofs/typing_ev.ml
@@ -146,5 +146,9 @@ let type_of env sigma c =
 (* The typed type of a judgment. *)
 
 let execute_type env sigma constr = 
-  let j = safe_machine env sigma constr in
+  let j = execute { fix=false; nocheck=true } env sigma constr in
+  assumption_of_judgment env sigma j
+
+let execute_type env sigma constr = 
+  let j = execute { fix=false; nocheck=false } env sigma constr in
   assumption_of_judgment env sigma j
diff --git a/proofs/typing_ev.mli b/proofs/typing_ev.mli
index f24ee3914a..b12cd369d3 100644
--- a/proofs/typing_ev.mli
+++ b/proofs/typing_ev.mli
@@ -13,3 +13,6 @@ open Evd
 val type_of : unsafe_env -> 'a evar_map -> constr -> constr
 
 val execute_type : unsafe_env -> 'a evar_map -> constr -> typed_type
+
+val execute_rec_type : unsafe_env -> 'a evar_map -> constr -> typed_type
+
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index 53b35ff6d1..04f96a8721 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -273,4 +273,20 @@ let explain_refiner_cannot_applt k ctx t harg =
        P.pr_term k ctx t; 'sPC; 'sTR"could not be applied to"; 'bRK(1,1);
        P.pr_term k ctx harg >]
 
+let error_occur_check ev rhs =
+  let id = "?" ^ string_of_int ev in
+  let pt = prterm rhs in
+  errorlabstrm "Trad.occur_check"
+    [< 'sTR"Occur check failed: tried to define "; 'sTR id;
+      'sTR" with term"; 'bRK(1,1); pt >]
+
+let error_not_clean sp t =
+  let c = Rel (List.hd (Listset.elements(free_rels t))) in
+  let id = string_of_id (Names.basename sp) in
+  let var = pTERM(c) in
+  errorlabstrm "Trad.not_clean"
+    [< 'sTR"Tried to define "; 'sTR id;
+       'sTR" with a term using variable "; var; 'sPC;
+       'sTR"which is not in its scope." >]
+
 end