Versions initiales

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

13 files changed, 2099 insertions, 0 deletions

diff --git a/pretyping/classops.ml b/pretyping/classops.ml
new file mode 100755
index 0000000000..667adca1b1
--- /dev/null
+++ b/pretyping/classops.ml
@@ -0,0 +1,392 @@
+
+
+open Std;;
+open Names;;
+open Vectops;;
+open Pp;;
+open Vartab;;
+open Libobject;;
+open Constrtypes;;
+open Vectops;;
+open List;;
+open Library;;
+open Term;;
+open More_util;;
+open Generic;;
+open Initial;;
+open Printer;;
+
+
+(* usage qque peu general: utilise aussi dans record *)
+
+type cte_typ = NAM_Var of identifier | NAM_SP of section_path | NAM_Construct of section_path*int*int
+;;
+
+let cte_of_constr = function  
+    (DOPN(Const sp,l)) -> NAM_SP sp
+  | (DOPN(MutInd (sp,_),l)) -> NAM_SP sp
+  | (VAR(id)) -> NAM_Var id
+  | (DOPN(MutConstruct ((sp,i),j) ,l)) -> NAM_Construct (sp,i,j)
+  |  _ -> raise Not_found
+;;
+
+type cl_typ = CL_SORT | CL_FUN | CL_Var of identifier | CL_SP of section_path 
+            | CL_IND of section_path*int
+;;
+
+type cl_info_typ = {cL_STR : string;
+                    cL_STRE : strength;
+                    cL_PARAM : int}
+;;
+
+type coe_typ = cte_typ
+;;
+
+type coe_info_typ = {cOE_VALUE : judgement;
+                     cOE_STRE : strength;
+                     cOE_ISID : bool;
+                     cOE_PARAM : int}
+;;
+
+type inheritance_path = int list
+;;
+
+(* table des classes, des coercions et graphe d'heritage *)
+
+let cLASSES = (ref [] : (int * (cl_typ * cl_info_typ)) list ref);;
+
+let cOERCIONS = (ref [] : (int * (coe_typ * coe_info_typ)) list ref);;
+
+let iNHERITANCE_GRAPH = (ref [] : ((int * int) * inheritance_path) list ref);; 
+
+let freeze () = (!cLASSES,!cOERCIONS,
+                 !iNHERITANCE_GRAPH)
+;;
+
+let unfreeze (fcl,fco,fig) = (cLASSES:=fcl;
+                              cOERCIONS:=fco;
+                              iNHERITANCE_GRAPH:=fig)
+;;
+
+(* ajout de nouveaux "objets" *)
+
+let newNum_class = 
+ let num = ref 0 in
+ function () -> (num:=!num+1;!num)
+;;
+
+let newNum_coercion = 
+ let num = ref 0 in
+ function () -> (num:=!num+1;!num)
+;;
+
+let add_new_class_num (n,(cl,s)) = 
+cLASSES := (n,(cl,s))::(!cLASSES)
+;;
+
+let add_new_class1 (cl,s) = 
+add_new_class_num (newNum_class(),(cl,s))
+;;
+
+let add_new_coercion_num (n,(coe,s)) = 
+cOERCIONS := (n,(coe,s))::(!cOERCIONS)
+;;
+
+let add_new_coercion (coe,s) = 
+let n = newNum_coercion() in 
+add_new_coercion_num (n,(coe,s));n
+;;
+
+let add_new_path x =
+iNHERITANCE_GRAPH := x::(!iNHERITANCE_GRAPH)
+;;
+
+let init () = (cLASSES:= []; 
+               add_new_class1 (CL_FUN,{cL_STR="FUNCLASS";cL_PARAM=0;cL_STRE=NeverDischarge});
+               add_new_class1 (CL_SORT,{cL_STR="SORTCLASS";cL_PARAM=0;cL_STRE=NeverDischarge});
+               cOERCIONS:= [];
+               iNHERITANCE_GRAPH:= [])
+;;
+
+init();;
+
+(* fonction de recherche *)
+
+let search_info x l = 
+let rec aux = function [] -> raise Not_found
+                     | (n,(x1,r))::l -> if x=x1 then (n,r)
+                                        else aux l
+in aux l
+;;
+
+(* class_info : cl_typ -> int * cl_info_typ *)
+
+let class_info cl = search_info cl (!cLASSES)
+;;
+
+(* class_info_from_index : int -> cl_typ * cl_info_typ *)
+
+let class_info_from_index i = List.assoc i (!cLASSES)
+;;
+
+(* coercion_info : coe_typ -> int * coe_info_typ *)
+
+let coercion_info coe = search_info coe (!cOERCIONS)
+;;
+
+(* coercion_info_from_index : int -> coe_typ * coe_info_typ *)
+
+let coercion_info_from_index i = List.assoc i (!cOERCIONS)
+;;
+
+let lookup_path_between (s,t) = List.assoc (s,t) (!iNHERITANCE_GRAPH);;
+
+let lookup_path_to_fun_from s = lookup_path_between (s,fst(class_info CL_FUN))
+;;
+
+let lookup_path_to_sort_from s = lookup_path_between (s,fst(class_info CL_SORT))
+;;
+
+
+(* library, summary *)
+
+(*val inClass : (cl_typ * cl_info_typ) -> Libobject.object = <fun>
+ val outClass : Libobject.object -> (cl_typ * cl_info_typ) = <fun> *)
+
+let (inClass,outClass) =
+    declare_object ("CLASS",
+                    {load_function = (fun _ -> ());
+                     cache_function = (function  (_,x) -> add_new_class1 x);
+                     specification_function = (function x -> x)});;
+
+let add_new_class (cl,s,stre,p) = 
+add_anonymous_object (inClass ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})))
+;;
+
+Library.declare_summary "inh_graph"
+{Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init}
+;;
+
+(* classe d'un terme *)
+
+(* constructor_at_head : constr -> cl_typ * int *)
+
+let constructor_at_head t = 
+let rec aux t' = match t' with
+    (DOPN(Const sp,_)) -> CL_SP sp,0
+  | (DOPN(MutInd (sp,i),_)) -> CL_IND (sp,i),0
+  | (VAR(id)) -> CL_Var id,0
+  | (DOP2(Cast,c,_)) -> aux (collapse_appl c)
+  | (DOPN(AppL,cl)) -> let c,_ = aux (hd_vect cl) 
+                        in c,Array.length(cl)-1
+  | DOP2(Prod,_,DLAM(_,c)) -> CL_FUN,0
+  | DOP0(Sort(_)) -> CL_SORT,0
+  |  _ -> raise Not_found
+in aux (collapse_appl t)
+;;
+
+(* class_of : Term.constr -> int *)
+
+
+let class_of sigma t = 
+let t,n,n1,i = (try let (cl,n) = constructor_at_head t in
+               let (i,{cL_PARAM=n1}) = class_info cl in
+               t,n,n1,i              
+              with _ -> let t = Reduction.hnf_constr sigma t in
+                        let (cl,n) = constructor_at_head t in
+                        let (i,{cL_PARAM=n1}) = class_info cl in
+                        t,n,n1,i) in
+if n = n1 then t,i 
+else raise Not_found
+;;
+
+(*
+
+let class_of t = 
+let (cl,n) = constructor_at_head t in
+let (i,{cL_PARAM=n1}) = class_info cl in
+if n = n1 then i 
+else raise Not_found
+;;
+*)
+
+let rec class_args_of c = 
+let aux = function (DOP2(Cast,c,_)) -> class_args_of c
+                 | (DOPN(AppL,cl)) -> Array.to_list(tl_vect(cl))
+                 | _ -> []
+in aux (collapse_appl c)
+;;
+
+(* verfications pour l'ajout d'une classe *)
+
+let fully_applied id p p1 =
+if p <> p1
+then  errorlabstrm "fully_applied" 
+          [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
+;;
+
+let rec arity_sort = function
+    DOP0(Sort(Prop(_))) -> 0
+  | DOP0(Sort(Type(_))) -> 0
+  | DOP2(Prod,_,DLAM(_,c)) -> (arity_sort c) +1
+  | DOP2(Cast,c,_) -> arity_sort c
+  | _ -> raise Not_found
+;;
+
+let stre_of_cl = 
+  function CL_SP sp ->
+                    (match Lib.leaf_object_tag (objsp_of sp) with
+                      "CONSTANT" ->
+                       let (_,stre,_) = Environ.outConstant(Lib.map_leaf (objsp_of sp)) in stre
+                      | _ -> NeverDischarge)
+          | CL_Var id -> stre_of_var id
+          | _ -> NeverDischarge
+;;
+
+(* coe_value : int -> Term.constr * bool *)
+
+let coe_value i = 
+let (_,{cOE_VALUE=v;cOE_ISID=b}) = coercion_info_from_index i in
+v,b
+;;
+
+(* fonction de print *)
+
+let string_of_strength = function NeverDischarge -> "(global)"
+                                | DischargeAt sp -> "(disch@"^(string_of_path sp)
+;;
+
+let print_coercion_value v = (prterm v.cOE_VALUE._VAL);;
+
+let print_index_coercion c = 
+ let _,v = coercion_info_from_index c in
+ print_coercion_value v;;
+
+(*
+let string_of_cl = function CL_Var id -> string_of_id id
+                          | CL_SP sp -> string_of_id (basename sp)
+                          | CL_IND (sp,i,s) -> s
+                          | CL_FUN -> "FUNCLASS"
+                          | CL_SORT -> "SORTCLASS";;
+*)
+
+let print_class i =
+ let cl,x = class_info_from_index i in
+ [< 'sTR x.cL_STR >];;
+
+let print_path ((i,j),p) = [< 'sTR"["; 
+                                   prlist_with_sep (fun () -> [< 'sTR"; " >])
+                                   (fun c ->  print_index_coercion c) p;
+                                   'sTR"] : "; print_class i; 'sTR" >-> ";
+                                   print_class j >];;
+
+let print_graph () = 
+  [< prlist_with_sep pr_fnl print_path (!iNHERITANCE_GRAPH) >];;
+
+let print_classes () = 
+  [< prlist_with_sep pr_spc
+     (fun (_,(cl,x)) -> 
+        [< 'sTR x.cL_STR  (*; 'sTR(string_of_strength x.cL_STRE) *) >]) 
+        (!cLASSES) >];;
+
+let print_coercions () = 
+  [< prlist_with_sep pr_spc
+     (fun (_,(_,v)) -> [< (print_coercion_value v)
+              (* ;'sTR(string_of_strength v.cOE_STRE)*) >]) (!cOERCIONS) >];;
+
+let cl_of_id id = 
+match (string_of_id id) with
+ "FUNCLASS" -> CL_FUN
+| "SORTCLASS" -> CL_SORT
+| _ -> let v = Machops.global (gLOB(initial_sign())) id in
+       let cl,_ = constructor_at_head v in cl
+;;
+
+let index_cl_of_id id =
+try let cl = cl_of_id id in
+    let i,_=class_info cl in i
+with _ -> errorlabstrm "index_cl_of_id"
+          [< 'sTR(string_of_id id); 'sTR" is not a defined class" >]
+;;
+
+let print_path_between ids idt = 
+let i = (index_cl_of_id ids) in
+let j = (index_cl_of_id idt) in
+let p = (try lookup_path_between (i,j) 
+         with _ -> errorlabstrm "index_cl_of_id"
+           [< 'sTR"No path between ";'sTR(string_of_id ids); 'sTR" and ";'sTR(string_of_id ids) >]) in
+print_path ((i,j),p);;
+
+(* rajouter une coercion dans le graphe *)
+ 
+let message_ambig l =
+    [< 'sTR"Ambiguous paths : ";
+       prlist_with_sep pr_fnl (fun ijp -> print_path ijp) l >];;
+
+(* add_coercion_in_graph : int * int * int -> unit 
+                         coercion,source,target *)
+
+let add_coercion_in_graph (ic,source,target) =
+let old_iNHERITANCE_GRAPH = (!iNHERITANCE_GRAPH) in
+let ambig_paths = (ref []:((int * int) * inheritance_path) list ref) in
+
+let try_add_new_path (p,i,j) =
+    try (if i=j 
+         then (if (snd (class_info_from_index i)).cL_PARAM > 0
+               then (lookup_path_between (i,j);
+                     ambig_paths := ((i,j),p)::!ambig_paths))
+         else
+          (lookup_path_between (i,j);
+          ambig_paths := ((i,j),p)::!ambig_paths);false)
+    with Not_found -> (add_new_path ((i,j),p);true)
+in
+let try_add_new_path1 (p,i,j) = (try_add_new_path (p,i,j);())
+in
+        (if try_add_new_path ([ic],source,target)
+           then 
+             (iter (fun ((s,t),p) ->
+                if s<>t 
+                then ((if (t = source)
+                       then begin
+                            try_add_new_path1 (p @ [ ic ],s,target);
+                            (iter (fun ((u,v),q) ->
+                                    if u<>v 
+                                    then if (u = target) & (p <> q)
+                                         then try_add_new_path1 (p @ [ ic ] @ q,s,v))
+                                              old_iNHERITANCE_GRAPH)
+                            end);
+                       if (s = target)
+                       then try_add_new_path1 (ic::p,source,t)))
+                 old_iNHERITANCE_GRAPH);
+
+if ((!ambig_paths) <> []) & is_mes_ambig()
+then pPNL (message_ambig (!ambig_paths)))
+;;
+
+
+let add_new_coercion_in_graph ((coef,xf),cls,clt) =
+let is,_ = class_info cls in
+let it,_ = class_info clt in
+let jf = add_new_coercion (coef,xf) in
+add_coercion_in_graph (jf,is,it)
+;;
+
+
+
+
+
+(* val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ  ->
+                    -> Libobject.object 
+   val outCoercion : Libobject.object -> (coe_typ * coe_info_typ) 
+                         * cl_typ * cl_typ *)
+
+let (inCoercion,outCoercion) =
+    declare_object ("COERCION",
+                    {load_function = (fun _ -> ());
+                     cache_function =
+                       (function  (_,x) -> add_new_coercion_in_graph x);
+                     specification_function = (function x -> x)});;
+
+
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
new file mode 100644
index 0000000000..98716046f2
--- /dev/null
+++ b/pretyping/classops.mli
@@ -0,0 +1,67 @@
+
+(* $Id$ *)
+
+(*i*)
+open Pp
+open Names
+open Term
+open Evd
+open Environ
+open Libobject
+open Declare
+(*i*)
+
+type cl_typ = 
+  | CL_SORT 
+  | CL_FUN 
+  | CL_Var of identifier 
+  | CL_SP of section_path
+  | CL_IND of section_path * int
+
+type cl_info_typ = {
+  cL_STR : string;
+  cL_STRE : strength;
+  cL_PARAM : int }
+
+type cte_typ = 
+  | NAM_Var of identifier 
+  | NAM_SP of section_path 
+  | NAM_Construct of section_path * int * int
+
+type coe_typ = cte_typ
+
+
+type coe_info_typ = {
+  cOE_VALUE : unsafe_judgment;
+  cOE_STRE : strength;
+  cOE_ISID : bool;
+  cOE_PARAM : int }
+
+
+type inheritance_path = int list
+
+
+val cte_of_constr : constr -> cte_typ
+val class_info : cl_typ -> (int * cl_info_typ)
+val coercion_info : coe_typ -> (int * coe_info_typ)
+val constructor_at_head : constr -> cl_typ * int
+val class_of :  'c evar_map -> constr -> constr * int
+val class_args_of : constr -> constr list
+val inClass : (cl_typ * cl_info_typ) -> obj
+val outClass : obj -> (cl_typ * cl_info_typ)
+val inCoercion : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> obj
+val outCoercion : obj -> (coe_typ * coe_info_typ) * cl_typ * cl_typ
+val lookup_path_between : (int * int) -> inheritance_path
+val lookup_path_to_fun_from : int -> inheritance_path
+val lookup_path_to_sort_from : int -> inheritance_path
+val coe_value : int -> (unsafe_judgment * bool)
+val print_graph : unit -> (int * string) Pp.ppcmd_token Stream.t
+val print_classes : unit -> (int * string) Pp.ppcmd_token Stream.t
+val print_coercions : unit -> (int * string) Pp.ppcmd_token Stream.t
+val print_path_between : identifier -> identifier -> (int * string) ppcmd_token Stream.t
+val arity_sort : constr -> int
+val fully_applied : identifier -> int -> int -> unit
+val stre_of_cl : cl_typ -> strength
+val add_new_class : (cl_typ * string * strength * int) -> unit
+val add_new_coercion_in_graph : (coe_typ * coe_info_typ) * cl_typ * cl_typ -> unit
+val add_coercion_in_graph : int * int * int -> unit
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
new file mode 100644
index 0000000000..07eb0fdc83
--- /dev/null
+++ b/pretyping/coercion.ml
@@ -0,0 +1,172 @@
+open Std;;
+open Generic;;
+open Names;;
+open Term;;
+open Reduction;;
+open Himsg;;
+open Machops;;
+open Mach;;
+open Classops;;
+open Recordops;;
+open Evarconv;;
+
+(* Typing operations dealing with coercions *)
+
+let class_of1 sigma t = class_of sigma (nf_ise1 sigma t);;
+
+let j_nf_ise sigma {_VAL=v;_TYPE=t;_KIND=k} =
+  {_VAL=nf_ise1 sigma v;_TYPE=nf_ise1 sigma t;_KIND=k}
+let jl_nf_ise sigma = List.map (j_nf_ise sigma)
+
+(* Here, funj is a coercion therefore already typed in global context *)
+let apply_coercion_args argl funj =
+  let rec apply_rec acc typ = function
+      [] -> {_VAL=applist(j_val_only funj,argl);
+             _TYPE= typ;
+             _KIND = funj._KIND}
+    | h::restl ->
+ (* On devrait pouvoir s'arranger pour qu'on ait pas à faire hnf_constr *)
+  match hnf_constr (Evd.mt_evd ()) typ with
+     DOP2(Prod,c1,DLAM(_,c2)) -> (* Typage garanti par l'appel a app_coercion*)
+       apply_rec (h::acc) (subst1 h c2) restl
+    | _ -> anomaly "apply_coercion_args"
+  in apply_rec [] funj._TYPE argl;;
+
+(* appliquer le chemin de coercions p a` hj *)
+
+let apply_pcoercion p hj typ_cl =
+  if !compter then
+    (nbpathc := !nbpathc +1; nbcoer := !nbcoer + (List.length p));
+  try fst (List.fold_left
+             (fun (ja,typ_cl) i -> 
+                let fv,b= coe_value i in
+                let argl = (class_args_of typ_cl)@[ja._VAL] in
+                let jres = apply_coercion_args argl fv in
+                  (if b then {_TYPE=jres._TYPE;_KIND=jres._KIND;_VAL=ja._VAL}
+                   else jres),jres._TYPE)
+             (hj,typ_cl) p)
+  with _ -> failwith "apply_pcoercion"
+
+let inh_app_fun isevars env j = 
+ match whd_betadeltaiota !isevars j._TYPE with
+    DOP2(Prod,_,DLAM(_,_)) -> j
+   | _ ->
+       (try
+ 	let t,i1 = class_of1 !isevars j._TYPE in
+      	let p = lookup_path_to_fun_from i1 in
+        apply_pcoercion p j t
+      with _ -> j)
+(* find out which exc we must trap (e.g we don't want to catch Sys.Break!) *)
+
+let inh_tosort_force isevars env j =
+  let t,i1 = class_of1 !isevars j._TYPE in
+  let p = lookup_path_to_sort_from i1 in
+  apply_pcoercion p j t 
+
+let inh_tosort isevars env j = 
+  let typ = whd_betadeltaiota !isevars j._TYPE in
+  match typ with
+    DOP0(Sort(_)) -> j  (* idem inh_app_fun *)
+  | _ -> (try inh_tosort_force isevars env j with _ -> j)
+
+let inh_ass_of_j isevars env j =
+   let typ = whd_betadeltaiota !isevars j._TYPE in
+     match typ with
+         DOP0(Sort s) -> {body=j._VAL;typ=s}
+       | _ ->
+           (try
+             let j1 = inh_tosort_force isevars env j
+             in assumption_of_judgement !isevars env j1 
+           with _ -> error_assumption CCI env (nf_ise1 !isevars j._VAL))
+                   (* try ... with _ -> ... is BAD *)
+
+let inh_coerce_to1 isevars env c1 v t k =
+ let t1,i1 = class_of1 !isevars c1 in
+ let t2,i2 = class_of1 !isevars t in
+ let p = lookup_path_between (i2,i1) in
+ let hj = {_VAL=v;_TYPE=t;_KIND=k} in
+ let hj' = apply_pcoercion p hj t2 in
+ if the_conv_x_leq isevars env hj'._TYPE c1 then hj'
+ else failwith "inh_coerce_to"
+
+let inh_coerce_to isevars env c1 hj =
+  inh_coerce_to1 isevars env c1 hj._VAL hj._TYPE hj._KIND
+
+let rec inh_conv_coerce1 isevars env c1 v t k =
+ if the_conv_x_leq isevars env t c1 
+ then {_VAL=v; _TYPE=t; _KIND=k}
+ else try inh_coerce_to1 isevars env c1 v t k
+ with _ ->  (* try ... with _ -> ... is BAD *)
+
+   (match (hnf_constr !isevars t,hnf_constr !isevars c1) with
+      | (DOP2(Prod,t1,DLAM(_,t2)),DOP2(Prod,u1,DLAM(name,u2))) -> 
+          let v' = hnf_constr !isevars v in
+            if (match v' with
+                    DOP2(Lambda,v1,DLAM(_,v2)) ->
+                      the_conv_x isevars env v1 u1 (* leq v1 u1? *)
+                  |         _                -> false)
+            then 
+	      let (x,v1,v2) = destLambda v' in
+(*              let jv1 = exemeta_rec def_vty_con isevars env v1 in 
+	      let assv1 = assumption_of_judgement !isevars env jv1 in
+ *)
+	      let assv1 = outcast_type v1 in
+              let env1 = add_rel (x,assv1) env in
+              let h2 = inh_conv_coerce1 isevars env1 u2 v2 t2 (mkSort (sort_of !isevars env1 t2)) in
+              abs_rel !isevars x assv1 h2
+            else 
+(*
+	      let ju1 = exemeta_rec def_vty_con isevars env u1 in 
+              let assu1 = assumption_of_judgement !isevars env ju1 in
+ *)
+	      let assu1 = outcast_type u1 in
+              let name = (match name with Anonymous -> Name (id_of_string "x")
+                            | _ -> name) in
+              let env1 = add_rel (name,assu1) env in
+              let h1 = 
+		inh_conv_coerce1 isevars env1 t1 (Rel 1) u1 (mkSort (level_of_type assu1)) in
+              let h2 = inh_conv_coerce1 isevars env1 u2  
+			 (DOPN(AppL,[|(lift 1 v);h1._VAL|])) 
+                         (subst1 h1._VAL t2) 
+			 (mkSort (sort_of !isevars env1 t2)) in
+	      abs_rel !isevars name assu1 h2
+      | _ -> failwith "inh_coerce_to")
+            
+let inh_conv_coerce isevars env c1 hj =
+  inh_conv_coerce1 isevars env c1 hj._VAL hj._TYPE hj._KIND
+
+let inh_cast_rel isevars env cj tj =
+    let cj' = (try inh_conv_coerce isevars env tj._VAL cj 
+              with Not_found | Failure _ -> error_actual_type CCI env 
+		  (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)) in
+      { _VAL = mkCast cj'._VAL tj._VAL;
+        _TYPE = tj._VAL;
+        _KIND = whd_betadeltaiota !isevars tj._TYPE}
+
+let inh_apply_rel_list nocheck isevars env argjl funj vtcon =
+  let rec apply_rec acc typ = function
+    [] -> let resj =
+      {_VAL=applist(j_val_only funj,List.map j_val_only (List.rev acc));
+       _TYPE= typ;
+       _KIND = funj._KIND} in
+      (match vtcon with 
+      | (_,(_,Some typ')) ->
+          (try inh_conv_coerce isevars env typ' resj
+          with _ -> resj) (* try ... with _ -> ... is BAD *)
+      | (_,(_,None)) -> resj)
+
+  | hj::restjl ->
+      match whd_betadeltaiota !isevars typ with
+          DOP2(Prod,c1,DLAM(_,c2)) ->
+            let hj' =
+              if nocheck then hj else 
+	      (try inh_conv_coerce isevars env c1 hj 
+               with (Failure _ | Not_found) ->
+                 error_cant_apply "Type Error" CCI env
+		   (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)) in
+            apply_rec (hj'::acc) (subst1 hj'._VAL c2) restjl
+        | _ ->
+            error_cant_apply "Non-functional construction" CCI env
+	      (j_nf_ise !isevars funj) (jl_nf_ise !isevars argjl)
+  in apply_rec [] funj._TYPE argjl
+;;
diff --git a/pretyping/coercion.mli b/pretyping/coercion.mli
new file mode 100644
index 0000000000..6cc815e49f
--- /dev/null
+++ b/pretyping/coercion.mli
@@ -0,0 +1,20 @@
+
+open Evd
+open Term
+open Sign
+open Environ
+open Evarutil
+
+
+val inh_app_fun : 'a evar_defs -> 'b -> unsafe_judgment -> unsafe_judgment
+val inh_tosort_force : 'a evar_defs -> 'b -> unsafe_judgment -> unsafe_judgment
+val inh_tosort : 'a evar_defs -> 'b -> unsafe_judgment -> unsafe_judgment
+val inh_ass_of_j : 'a evar_defs -> var_context ->
+  unsafe_judgment -> typed_type
+val inh_coerce_to : 'a evar_defs -> var_context ->
+  constr -> unsafe_judgment -> unsafe_judgment
+val inh_cast_rel : 'a evar_defs -> var_context ->
+  unsafe_judgment -> unsafe_judgment -> unsafe_judgment
+val inh_apply_rel_list : bool -> 'a evar_defs -> var_context ->
+  unsafe_judgment list -> unsafe_judgment -> 'b * ('c * constr option) 
+    -> unsafe_judgment
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
new file mode 100644
index 0000000000..83d38efa22
--- /dev/null
+++ b/pretyping/evarconv.ml
@@ -0,0 +1,308 @@
+
+(* $Id$ *)
+
+open Util
+open Names
+open Generic
+open Term
+open Reduction
+open Classops
+open Recordops 
+open Evarutil
+
+(* Pb: Mach cannot type evar in the general case (all Const must be applied
+ * to VARs). But evars may be applied to Rels or other terms! This is the
+ * difference between type_of_const and type_of_const2.
+ *)
+(* 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
+(* FIN TMP ***** *)
+
+
+(* This code (i.e. try_solve_pb, solve_pb, etc.) takes a unification
+ * problem, and tries to solve it. If it solves it, then it removes
+ * all the conversion problems, and re-runs conversion on each one, in
+ * the hopes that the new solution will aid in solving them.
+ *
+ * The kinds of problems it knows how to solve are those in which
+ * the usable arguments of an existential var are all themselves
+ * universal variables.
+ * The solution to this problem is to do renaming for the Var's,
+ * to make them match up with the Var's which are found in the
+ * hyps of the existential, to do a "pop" for each Rel which is
+ * not an argument of the existential, and a subst1 for each which
+ * is, again, with the corresponding variable. This is done by
+ * Tradevar.evar_define
+ *
+ * Thus, we take the arguments of the existential which we are about
+ * to assign, and zip them with the identifiers in the hypotheses.
+ * Then, we process all the Var's in the arguments, and sort the
+ * Rel's into ascending order.  Then, we just march up, doing
+ * subst1's and pop's.
+ *
+ * NOTE: We can do this more efficiently for the relative arguments,
+ * by building a long substituend by hand, but this is a pain in the
+ * 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 conversion_problems = ref ([] : (conv_pb * constr * constr) list)
+
+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
+      (fun (pbs,pbs1) pb ->
+    	if status_changed lsp pb then (pb::pbs,pbs1)
+        else (pbs,pb::pbs1))
+      ([],[])
+      !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 =
+  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 ->
+	 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
+
+
+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
+    c,bs,(xs,xs1),(us,us1),(ts,ts1),t
+  with _ -> raise Not_found  (* try ... with _ -> ... *)
+
+
+
+let the_conv_x isevars env t1 t2 =
+  conv_x !isevars t1 t2 or evar_conv_x isevars (Some env) CONV_X 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     
+ 
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index cab7a15d2f..0a44a9553e 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -1,2 +1,22 @@
 
 (* $Id$ *)
+
+(*i*)
+open Term
+open Sign
+open Environ
+open Reduction
+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
+
+
+(* 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
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
new file mode 100644
index 0000000000..64a2dd9d1a
--- /dev/null
+++ b/pretyping/evarutil.ml
@@ -0,0 +1,492 @@
+(****************************************************************************)
+(*                 The Calculus of Inductive Constructions                  *)
+(*                                                                          *)
+(*                                Projet Coq                                *)
+(*                                                                          *)
+(*                     INRIA        LRI-CNRS        ENS-CNRS                *)
+(*              Rocquencourt         Orsay          Lyon                    *)
+(*                                                                          *)
+(*                                 Coq V6.3                                 *)
+(*                               July 1st 1999                              *)
+(*                                                                          *)
+(****************************************************************************)
+(*                               tradevar.ml                                *)
+(****************************************************************************)
+
+open Std;;
+open Pp;;
+open Names;;
+open Impuniv;;
+open Vectops;;
+open Generic;;
+open Term;;
+open Printer;;
+open Termenv;;
+open Evd;;
+open Reduction;;
+open Himsg;;
+
+
+let rec filter_unique = function
+    [] -> []
+  | x::l ->
+      if List.mem x l then filter_unique (filter (fun y -> x<>y) l)
+      else x::filter_unique l
+;;
+
+let distinct_id_list = 
+  let rec drec fresh = function
+      [] -> List.rev fresh 
+    | id::rest ->
+ 	let id' = next_ident_away_from id fresh in drec (id'::fresh) rest
+  in drec []
+;;
+
+let filter_sign p sign x =
+  sign_it
+    (fun id ty (v,ids,sgn) ->
+      let (disc,v') = p v (id,ty) in
+      if disc then (v', id::ids, sgn) else (v', ids, add_sign (id,ty) sgn))
+    sign
+    (x,[],nil_sign)
+;;
+
+
+(*------------------------------------*
+ * functional operations on evar sets *
+ *------------------------------------*)
+
+(* All ids of sign must be distincts! *)
+let new_isevar_sign env sigma typ args k =
+  let sign = context env in
+  (if not (distinct (ids_of_sign sign))
+  then error "new_isevar_sign: two vars have the same name");
+  let newsp = new_isevar_path k in
+  (Evd.add_noinfo sigma newsp sign typ, mkConst newsp 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;;
+
+(* Declaring any type to be in the sort Type shouldn't be harmful since
+   cumulativity now includes Prop and Set in Type. *)
+let new_type_var sigma sign k =
+  let args = (Array.of_list (List.map mkVar (ids_of_sign sign))) in
+  let (sigma',c) = new_isevar_sign sigma sign dummy_sort args k in
+  (sigma', make_type c (Type dummy_univ))
+;;
+
+let split_evar_to_arrow sigma c =
+  let (sp,args) = destConst c in
+  let k = kind_of_path sp in
+  let evd = Evd.map sigma sp in
+  let hyps= evd.hyps in
+  let (sigma1,dom) = new_type_var sigma hyps k in
+  let nvar = next_ident_away (id_of_string "x") (ids_of_sign hyps) in
+  let nhyps = add_sign (nvar,dom) hyps in
+  let (sigma2,rng) = new_type_var sigma1 nhyps k in
+  let prod = Environ.prod_create (incast_type dom, 
+				  subst_var nvar (body_of_type rng)) in
+  let sigma3 = Evd.define sigma2 sp prod in
+  let dsp = path_of_const (body_of_type dom) in
+  let rsp = path_of_const (body_of_type rng) in
+  (sigma3,
+   mkCast (mkConst dsp args) dummy_sort,
+   mkCast (mkConst rsp (cons_vect (mkRel 1) args)) dummy_sort)
+;;
+
+(* Redefines an evar with a smaller context (i.e. it may depend on less
+ * variables) such that c becomes closed.
+ * Example: in [x:?1; y:(list ?2)] <?3>x=y /\ x=(nil bool)
+ * ?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.
+ *)
+let do_restrict_hyps sigma c =
+  let (sp,argsv) = destConst c in
+  let k = kind_of_path sp in
+  let args = Array.to_list argsv in
+  let evd = Evd.map sigma sp in
+  let hyps= evd.hyps 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)))
+;;
+
+
+
+(*------------------------------------*
+ * operations on the evar constraints *
+ *------------------------------------*)
+
+type 'a evar_defs = 'a Evd.evar_map ref
+
+(* ise_try [f1;...;fn] tries fi() for i=1..n, restoring the evar constraints
+ * when fi returns false or an exception. Returns true if one of the fi
+ * returns true, and false if every fi return false (in the latter case,
+ * the evar constraints are restored).
+ *)
+let ise_try isevars l =
+  let u = !isevars in
+  let rec test = function
+      [] -> isevars := u; false
+    | f::l ->
+ 	  (try f() with reraise -> isevars := u; raise reraise)
+       or (isevars := u; test l)
+  in test l
+;;
+
+
+(* say if the section path sp corresponds to an existential *)
+let ise_in_dom isevars sp = Evd.in_dom !isevars sp;;
+
+(* map the given section path to the evar_declaration *)
+let ise_map isevars sp = Evd.map !isevars sp;;
+
+(* define the existential of section path sp as the constr body *)
+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)
+  | _ -> false
+;;
+
+let ise_defined isevars k =
+  match k with
+    DOPN(Const _,_) -> Termenv.defined_existential !isevars k
+  | _ -> false
+;;
+
+let restrict_hyps isevars c =
+  if ise_undefined isevars c & not (closed0 c)
+  then
+    (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." >]
+;;
+
+(* We try to instanciate the evar assuming the body won't depend
+ * on arguments that are not Rels or VARs, or appearing several times.
+ *)
+(* Note: error_not_clean should not be an error: it simply means that the
+ * conversion test that lead to the faulty call to [real_clean] should return
+ * false. The problem is that we won't get the right error message.
+ *)
+let real_clean isevars sp args rhs =
+  let subst = List.map (fun (x,y) -> (y,VAR x)) (filter_unique args) in
+  let rec subs k t =
+    match t with
+      Rel i ->
+ 	if i<=k then t
+ 	else (try List.assoc (Rel (i-k)) subst with Not_found -> t)
+    | VAR _ -> (try List.assoc t subst with Not_found -> t)
+    | DOP0 _ -> t
+    | DOP1(o,a) -> DOP1(o, subs k a)
+    | DOP2(o,a,b) -> DOP2(o, subs k a, subs k b)
+    | DOPN(o,v) -> restrict_hyps isevars (DOPN(o, Array.map (subs k) v))
+    | DOPL(o,l) -> DOPL(o, List.map (subs k) l)
+    | 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;
+  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 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))))) ->
+	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
+  let (sign',typ') = aux sign (List.length dbenv, t) 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
+  isevars := sigma';
+  (evar,typ')
+;;
+
+
+(* [evar_define] solves the problem lhs = rhs when lhs is an uninstantiated
+ * evar, i.e. tries to find the body ?sp for lhs=DOPN(Const sp,args)
+ * ?sp [ sp.hyps \ args ]  unifies to rhs
+ * ?sp must be a closed term, not referring to itself.
+ * Not so trivial because some terms of args may be terms that are not
+ * variables. In this case, the non-var-or-Rels arguments are replaced
+ * by <implicit>. [clean_rhs] will ignore this part of the subtitution. 
+ * This leads to incompleteness (we don't deal with pbs that require
+ * inference of dependent types), but it seems sensible.
+ *
+ * If after cleaning, some free vars still occur, the function [restrict_hyps]
+ * tries to narrow the env of the evars that depend on Rels.
+ *
+ * If after that free Rels still occur it means that the instantiation
+ * cannot be done, as in  [x:?1; y:nat; z:(le y y)] x=z
+ * ?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 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
+  (* 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]
+;;
+
+
+(* 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).
+ *)
+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
+      (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
+  let nsign = rev_sign rsign in
+  let nargs = (Array.of_list (List.map mkVar (ids_of_sign nsign))) in
+  let newsp = new_isevar_path CCI in
+  isevars :=
+    Evd.define (Evd.add_noinfo !isevars newsp nsign evd.Evd.concl)
+      sp (mkConst newsp nargs);
+  Some [sp]
+
+
+(* 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.
+ *)
+(* 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
+;;
+
+(*-------------------*)
+(* Now several auxiliary functions for the conversion algorithms modulo
+ * evars. used in trad and progmach
+ *)
+
+
+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)
+    
+;;
+
+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 is_eliminator = function
+    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
+;;
+
+
+
+(* 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
+ *   (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 constraint *)
+let mt_tycon = (false,(None,None));;
+
+(* The default constraints for types. *)
+let def_vty_con = (true,(None,None));;
+
+(* Constrain only the type *)
+let mk_tycon ty = (false,(None,Some ty));;
+let mk_tycon2 (is_ass,_) ty = (is_ass,(None,Some ty))
+
+
+(* Propagation of constraints through application and abstraction *)
+
+(* 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)
+;;
+
+(* 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))
+;;
+
+(* 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)
+;;
+
+(* 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))
+;;
+
+(* Given a constraint on an abstraction, returns the constraint on the body *)
+let abs_rng_tycon isevars = function
+    (_,(_,None)) -> mt_tycon
+  | (_,(_,Some c)) ->
+      (match whd_betadeltaiota !isevars c with
+      | DOP2(Prod,_,DLAM(_,b)) -> mk_tycon b
+      | _ -> mt_tycon)
+;;
+
+(* $Id$ *)
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli
index cab7a15d2f..d7ef3620fb 100644
--- a/pretyping/evarutil.mli
+++ b/pretyping/evarutil.mli
@@ -1,2 +1,68 @@
 
+(* This modules provides useful functions for unification algorithms.
+ * Used in Trad and Progmach
+ * This interface will have to be improved.
+ *)
+
+open Names
+open Term
+open Sign
+open Evd
+open Environ
+open Reduction
+
+val filter_unique : 'a list -> 'a list
+val distinct_id_list : identifier list -> identifier list
+
+val filter_sign :
+  ('a -> identifier * typed_type -> bool * 'a) -> var_context -> 'a ->
+  'a * identifier list * var_context
+
+val dummy_sort : constr
+val do_restrict_hyps : 'a evar_map -> constr -> 'a evar_map * constr
+
+
+type 'a evar_defs = 'a evar_map ref
+
+val ise_try : 'a evar_defs -> (unit -> bool) list -> bool
+
+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
+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
+
+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
+
+
+(* Value/Type constraints *)
+
+type trad_constraint = bool * (constr option * constr option)
+
+val mt_tycon : trad_constraint
+val def_vty_con : trad_constraint
+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_rng_tycon :
+  '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
+
+
 (* $Id$ *)
diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml
new file mode 100644
index 0000000000..ea958976bd
--- /dev/null
+++ b/pretyping/pretype_errors.ml
@@ -0,0 +1,6 @@
+
+let error_cant_find_case_type loc env expr =
+  raise (PretypeError (loc,CCI,context env,CantFindCaseType expr))
+
+let error_ill_formed_branch k env c i actty expty =
+  raise (TypeError (k, context env, IllFormedBranch (c,i,actty,expty)))
diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli
new file mode 100644
index 0000000000..2356154989
--- /dev/null
+++ b/pretyping/pretype_errors.mli
@@ -0,0 +1,22 @@
+
+(* $Id$ *)
+
+open Pp
+open Names
+open Term
+open Sign
+open Environ
+open Type_errors
+open Rawterm
+
+(* The type of errors raised by the pretyper *)
+
+exception PreTypeError of loc * path_kind * context * type_error
+
+val error_cant_find_case_type_loc : loc -> unsafe_env -> constr -> 'a
+
+val error_number_branches_loc : 
+  loc -> unsafe_env -> constr -> constr -> int -> 'b
+
+val error_ill_formed_branch_loc : 
+  loc -> path_kind -> unsafe_env -> constr -> int -> constr -> constr -> 'b
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
new file mode 100644
index 0000000000..7fa60737d0
--- /dev/null
+++ b/pretyping/pretyping.ml
@@ -0,0 +1,360 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Sign
+open Evd
+open Term
+open Reduction
+open Environ
+open Type_errors
+open Typeops
+open Classops
+open List
+open Recordops 
+open Evarutil
+open Pretype_errors
+open Rawterm
+open Evarconv
+open Coercion
+
+let ctxt_of_ids ids =
+  Array.of_list (List.map (function id -> VAR id) ids)
+
+let mt_evd = Evd.empty
+
+let vect_lift_type = Array.mapi (fun i t -> typed_app (lift i) t)
+
+let j_nf_ise env sigma {uj_val=v;uj_type=t;uj_kind=k} =
+  {uj_val=nf_ise1 env sigma v;uj_type=nf_ise1 env sigma t;uj_kind=k}
+
+let jv_nf_ise env sigma = Array.map (j_nf_ise env sigma)
+
+let evar_type_fixpoint env isevars lna lar vdefj =
+  let lt = Array.length vdefj in 
+    if Array.length lar = lt then 
+      for i = 0 to lt-1 do 
+        if not (the_conv_x_leq env isevars
+		  (vdefj.(i)).uj_type (lift lt (body_of_type lar.(i)))) then
+          error_ill_typed_rec_body CCI env i lna 
+	    (jv_nf_ise env !isevars vdefj) 
+	    (Array.map (typed_app (nf_ise1 env !isevars)) lar)
+      done
+
+
+(* Inutile ?
+let cast_rel isevars env cj tj =
+    if the_conv_x_leq isevars env cj.uj_type tj.uj_val then
+        {uj_val=j_val_only cj;
+         uj_type=tj.uj_val;
+         uj_kind = hnf_constr !isevars tj.uj_type}
+   else error_actual_type CCI env (j_nf_ise !isevars cj) (j_nf_ise !isevars tj)
+
+*)
+let let_path = make_path ["Core"] (id_of_string "let") CCI
+
+let wrong_number_of_cases_message loc env isevars (c,ct) expn = 
+  let c = nf_ise1 env !isevars c and ct = nf_ise1 env !isevars ct in
+  error_number_branches_loc loc env c ct expn
+
+let check_branches_message loc env isevars (c,ct) (explft,lft) = 
+  let n = Array.length explft and expn = Array.length lft in
+  if n<>expn then wrong_number_of_cases_message loc env isevars (c,ct) expn;
+  for i = 0 to n-1 do
+    if not (the_conv_x_leq env isevars lft.(i) explft.(i)) then 
+      let c = nf_ise1 env !isevars c
+      and ct = nf_ise1 env !isevars ct 
+      and lfi = nf_betaiota env !isevars (nf_ise1 env !isevars lft.(i)) in
+      error_ill_formed_branch_loc loc CCI env c i lfi (nf_betaiota env !isevars explft.(i))
+  done
+
+(*
+let evar_type_case isevars env ct pt lft p c =
+  let (mind,bty,rslty) = type_case_branches env !isevars ct pt p c
+  in check_branches_message isevars env (c,ct) (bty,lft); (mind,rslty)
+*)
+
+
+let trad_metamap = ref []
+let trad_nocheck = ref false
+
+let pretype_ref loc isevars env = function
+| RMeta n ->
+    let metaty =
+      try List.assoc n !trad_metamap
+      with Not_found ->
+	Ast.user_err_loc 
+	  (loc,"pretype",
+	   [< 'sTR "Metavariable "; 'iNT n; 'sTR "remains non instanciated" >])
+	  in
+    (match kind_of_term metaty with
+      IsCast (typ,kind) -> {uj_val=DOP0 (Meta n); uj_type=typ; uj_kind=kind}
+    | _ ->
+        {uj_val=DOP0 (Meta n);
+          uj_type=metaty;
+          uj_kind=failwith "should be casted"})
+	   (* hnf_constr !isevars (exemeta_hack metaty).uj_type}) *)
+
+| RVar id ->
+    let {body=typ;typ=s} = snd(lookup_glob id (context env)) in
+    {uj_val=VAR id; uj_type=typ; uj_kind = DOP0 (Sort s)}
+
+| RConst (sp,ids) ->
+    let cstr = mkConst sp (ctxt_of_ids ids) in
+    make_judge cstr (type_of_constant env !isevars cstr)
+(*
+| RAbst sp ->
+  if sp = let_path then
+      (match Array.to_list cl with
+       [m;DLAM(na,b)] ->
+       let mj = pretype mt_tycon isevars env m in
+	 (try 
+	    let mj = inh_ass_of_j isevars env mj in
+	    let mb = body_of_type mj in
+	    let bj =
+	     pretype mt_tycon isevars (add_rel (na,mj) env) b in
+	   {uj_val = DOPN(Abst sp,[|mb;DLAM(na,bj.uj_val)|]);
+            uj_type = sAPP (DLAM(na,bj.uj_type)) mb;
+            uj_kind = pop bj.uj_kind }
+	 with UserError _ -> 
+	   pretype vtcon isevars env (abst_value cstr)) 
+      | _ -> errorlabstrm "Trad.constr_of_com" [< 'sTR"Malformed ``let''" >])
+   else if evaluable_abst cstr then
+     pretype vtcon isevars env (abst_value cstr)
+   else error "Cannot typecheck an unevaluable abstraction"
+*)
+
+| REVar (sp,ids) ->
+    let cstr = mkConst sp (ctxt_of_ids ids) in
+    make_judge cstr (type_of_existential env !isevars cstr)
+
+| RInd ((sp,i),ids) ->
+    let cstr = mkMutInd sp i (ctxt_of_ids ids) in
+    make_judge cstr (type_of_inductive env !isevars cstr)
+ 
+| RConstruct (((sp,i),j),ids) ->
+    let cstr = mkMutConstruct sp i j (ctxt_of_ids ids) in
+    let (typ,kind) = destCast (type_of_constructor env !isevars cstr) in
+    {uj_val=cstr; uj_type=typ; uj_kind=kind}
+
+(* pretype vtcon isevars env constr tries to solve the *)
+(* existential variables in constr in environment env with the *)
+(* constraint vtcon (see Tradevar). *)
+(* Invariant : Prod and Lambda types are casted !! *)
+let rec pretype vtcon env isevars cstr =
+match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
+
+
+| RRef (loc,ref) -> 
+    pretype_ref loc isevars env ref
+
+| RRel (loc,n) -> relative env n
+
+| RHole loc ->
+  if !compter then nbimpl:=!nbimpl+1;
+  (match vtcon with
+    (true,(Some v, _)) ->
+      let (valc,typc) = destCast v in
+      {uj_val=valc; uj_type=typc; uj_kind=dummy_sort}
+  | (false,(None,Some ty)) ->
+      let (c,ty) = new_isevar env isevars ty CCI in
+      {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
+  | (true,(None,None)) ->
+      let (c,ty) = new_isevar env isevars (mkCast dummy_sort dummy_sort) CCI in
+      {uj_val=c;uj_type=ty;uj_kind = dummy_sort}
+  | (false,(None,None)) ->
+      (match loc with
+	  None -> anomaly "There is an implicit argument I cannot solve"
+	| Some loc -> 
+	    Ast.user_err_loc
+	      (loc,"pretype",
+	       [< 'sTR "Cannot infer a term for this placeholder" >]))
+  | _ -> anomaly "tycon")
+
+
+| RRec (loc,fixkind,lfi,lar,vdef) ->
+  let larj = Array.map (pretype def_vty_con env isevars) lar in
+  let lara = Array.map (assumption_of_judgment env !isevars) larj in
+  let nbfix = Array.length lfi in
+  let lfi = List.map (fun id -> Name id) (Array.to_list lfi) in
+  let newenv =
+    array_fold_left2 (fun env id ar -> (push_rel (id,ar) env))
+      env (Array.of_list (List.rev lfi)) (vect_lift_type lara) in
+  let vdefj =
+    Array.mapi 
+      (fun i def -> (* we lift nbfix times the type in tycon, because of
+                     * the nbfix variables pushed to newenv *)
+        pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars def)
+      vdef in
+  (evar_type_fixpoint env isevars lfi lara vdefj;
+  match fixkind with
+    | RFix(vn,i) ->
+      let fix = mkFix vn i lara (List.rev lfi) (Array.map j_val_only vdefj) in
+	check_fix env !isevars fix;
+	make_judge fix lara.(i)
+    | RCofix i -> 
+      let cofix = mkCoFix i lara (List.rev lfi) (Array.map j_val_only vdefj) in
+	check_cofix env !isevars cofix;
+	make_judge cofix lara.(i))
+
+| RSort (loc,RProp c) -> make_judge_of_prop_contents c
+
+| RSort (loc,RType) -> 
+    { uj_val = dummy_sort; uj_type = dummy_sort; uj_kind = dummy_sort }
+
+| RApp (loc,f,args) -> 
+    let j = pretype mt_tycon env isevars f in
+    let j = inh_app_fun env isevars j in
+    let apply_one_arg (tycon,jl) c =
+      let cj = pretype (app_dom_tycon isevars tycon) env isevars c in
+      let rtc = app_rng_tycon isevars cj.uj_val tycon in
+      (rtc,cj::jl)  in
+    let jl = List.rev (snd (List.fold_left apply_one_arg
+			      (mk_tycon j.uj_type,[]) args)) in
+    inh_apply_rel_list !trad_nocheck env isevars jl j vtcon
+
+| RBinder(loc,BLambda,name,c1,c2)      ->
+    let j = pretype (abs_dom_valcon isevars vtcon) env isevars c1 in
+    let assum = inh_ass_of_j env isevars j in
+    let var = (name,assum) in
+    let j' =
+      pretype (abs_rng_tycon isevars vtcon) isevars
+ 	(add_rel var env) c2 in 
+    abs_rel !isevars name assum j'
+
+| RBinder(loc,BProd,name,c1,c2)        ->
+    let j = pretype def_vty_con env isevars c1 in
+    let assum = inh_ass_of_j env isevars j in
+    let var = (name,assum) in
+    let j' = pretype def_vty_con isevars (add_rel var env) c2 in
+    let j'' = inh_tosort env isevars j' in
+    gen_rel !isevars CCI env name assum j''
+
+| ROldCase (loc,isrec,po,c,lf) ->
+  let cj = pretype mt_tycon env isevars c in
+  let (mind,_) =
+    try find_mrectype !isevars cj.uj_type
+    with Induc -> error_case_not_inductive CCI env
+	(nf_ise1 !isevars cj.uj_val) (nf_ise1 !isevars cj.uj_type) in
+  let pj = match po with
+    | Some p -> pretype mt_tycon env isevars p
+    | None -> 
+	try match vtcon with
+	    (_,(_,Some pred)) -> 
+	      let (predc,predt) = destCast pred in
+	      let predj = {uj_val=predc;uj_type=predt;uj_kind=dummy_sort} in
+	      inh_tosort env isevars predj
+	  | _ -> error "notype"
+	with UserError _ -> (* get type information from type of branches *)
+	  let rec findtype i =
+	    if i > Array.length lf
+	    then error_cant_find_case_type loc env cj.uj_val
+	    else
+	      try
+		let expti = Indrec.branch_scheme !isevars isrec i cj.uj_type in
+		let fj = pretype (mk_tycon expti) env isevars lf.(i-1) in
+		let efjt = nf_ise1 !isevars fj.uj_type in 
+		let pred = 
+		  Indrec.pred_case_ml_onebranch env !isevars isrec 
+		    (cj.uj_val,cj.uj_type) (i,fj.uj_val,efjt) in
+		if has_ise pred then findtype (i+1)
+		else 
+		  let pty = Mach.newtype_of env !isevars pred in
+		    {uj_val=pred;uj_type=pty;uj_kind=Mach.newtype_of env !isevars pty}
+	      with UserError _ -> findtype (i+1) in
+	    findtype 1 in
+
+  let evalct = nf_ise1 !isevars cj.uj_type
+  and evalPt = nf_ise1 !isevars pj.uj_type in
+
+  let (mind,bty,rsty) =
+    Indrec.type_rec_branches isrec env !isevars evalct evalPt pj.uj_val cj.uj_val in
+  if Array.length bty <> Array.length lf then
+    wrong_number_of_cases_message loc env isevars (cj.uj_val,evalct)
+      (Array.length bty)
+  else
+    let lfj =
+      map2_vect
+        (fun tyc f -> pretype (mk_tycon tyc) env isevars f) bty lf in
+    let lft = (Array.map (fun j -> j.uj_type) lfj) in
+    check_branches_message loc env isevars (cj.uj_val,evalct) (bty,lft);
+    let v =
+      if isrec
+      then 
+	let rEC = Array.append [|(j_val pj); (j_val cj)|]
+		    (Array.map j_val lfj) in
+	Indrec.transform_rec loc env !isevars rEC (evalct,evalPt)
+      else let ci = ci_of_mind mind in
+	mkMutCaseA ci (j_val pj) (j_val cj) (Array.map j_val lfj) in
+
+      {uj_val = v;
+       uj_type = rsty;
+       uj_kind = sort_of_arity !isevars evalPt}
+
+| RCases (loc,prinfo,po,tml,eqns) ->
+    Multcase.compile_multcase
+      ((fun vtyc -> pretype vtyc isevars),isevars)
+      vtcon env (po,tml,eqns)
+(*
+| DOP2(Cast,c,t) ->
+  let tj = pretype def_vty_con env isevars t in
+  let tj = inh_tosort_force env isevars tj in
+  let cj =
+    pretype (mk_tycon2 vtcon (assumption_of_judgement env !isevars tj).body)
+      env isevars c in
+  inh_cast_rel env isevars cj tj
+*)
+(* Maintenant, tout s'exécute... 
+  | _ -> error_cant_execute CCI env (nf_ise1 !isevars cstr)
+*)
+
+
+let unsafe_fmachine vtcon nocheck isevars metamap env constr = 
+  trad_metamap := metamap;
+  trad_nocheck := nocheck;
+  reset_problems ();
+  pretype vtcon env isevars constr
+
+
+(* [fail_evar] says how to process unresolved evars:
+ *   true -> raise an error message
+ *   false -> convert them into new Metas (casted with their type)
+ *)
+let process_evars fail_evar sigma =
+  (if fail_evar then whd_ise sigma else whd_ise1_metas sigma)
+
+
+let j_apply f j = 
+  { uj_val=strong (under_outer_cast f) j.uj_val;
+    uj_type=strong f j.uj_type;
+    uj_kind=strong f j.uj_kind}
+
+(* TODO: comment faire remonter l'information si le typage a resolu des
+       variables du sigma original. il faudrait que la fonction de typage
+       retourne aussi le nouveau sigma...
+*)
+let ise_resolve fail_evar sigma metamap env c =
+  let isevars = ref sigma in
+  let j = unsafe_fmachine mt_tycon false isevars metamap env c in
+  j_apply (process_evars fail_evar !isevars) j
+
+
+let ise_resolve_type fail_evar sigma metamap env c =
+  let isevars = ref sigma in
+  let j = unsafe_fmachine def_vty_con false isevars metamap env c in
+  let tj = inh_ass_of_j env isevars j in
+  type_app (strong (process_evars fail_evar !isevars)) tj
+
+
+let ise_resolve_nocheck sigma metamap env c =
+  let isevars = ref sigma in
+  let j = unsafe_fmachine mt_tycon true isevars metamap env c in
+  j_apply (process_evars true !isevars) j
+
+
+let ise_resolve1 is_ass sigma env c =
+  if is_ass then body_of_type (ise_resolve_type true sigma [] env c)
+  else (ise_resolve true sigma [] env c).uj_val
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
new file mode 100755
index 0000000000..07833ae20e
--- /dev/null
+++ b/pretyping/recordops.ml
@@ -0,0 +1,126 @@
+
+open Std;;
+open Names;;
+open Machops;;
+open Vectops;;
+open Himsg;;
+open Pp;;
+open Vartab;;
+open Libobject;;
+open Vectops;;
+open List;;
+open Library;;
+open Term;;
+open More_util;;
+open Pp_control;;
+open Generic;;
+open Initial;;
+open Classops;;
+
+
+let nbimpl = ref 0;;
+let nbpathc = ref 0;;
+let nbcoer = ref 0;;
+let nbstruc = ref 0;;
+let nbimplstruc = ref 0;;
+
+let compter = ref false;;
+
+
+(*** table des structures: section_path du struc donne l'id du constructeur,
+     le nombre de parame`tres et ses projection valides ***)
+
+type struc_typ = {s_CONST : identifier; 
+                  s_PARAM : int;
+                  s_PROJ : section_path option list};;
+
+let sTRUCS = (ref [] : (section_path * struc_typ) list ref);;
+
+let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
+;;
+
+let (inStruc,outStruc) =
+    declare_object ("STRUCTURE",
+                    {load_function = (fun _ -> ());
+                     cache_function = (function  (_,x) -> add_new_struc1 x);
+                     specification_function = (function x -> x)});;
+
+let add_new_struc (s,c,n,l) = 
+add_anonymous_object (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
+;;
+
+let struc_info s = assoc s !sTRUCS
+;;
+
+(*** table des definitions "object" : pour chaque object c,
+c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n)
+ avec ti=(ci ui1...uir)
+      
+Pour tout ci, et Li correspondant (du record)
+     o_DEF = c
+     o_TABS = B1...Bk
+     o_PARAMS = a1...am
+     o_TCOMP = ui1...uir
+***)
+
+type obj_typ = {o_DEF : constr;
+                o_TABS : constr list; (* dans l'ordre *)
+                o_TPARAMS : constr list; (* dans l'ordre *)
+                o_TCOMPS : constr list (* dans l'ordre *)
+               };;
+
+let oBJDEFS = (ref [] : ((cte_typ*cte_typ) * obj_typ) list ref);;
+
+let add_new_objdef1 x = oBJDEFS:=x::(!oBJDEFS)
+;;
+
+let (inObjDef,outObjDef) =
+    declare_object ("OBJDEF",
+                    {load_function = (fun _ -> ());
+                     cache_function = (function  (_,x) -> add_new_objdef1 x);
+                     specification_function = (function x -> x)});;
+
+let add_new_objdef (o,c,la,lp,l) =
+  try let _ = assoc o !oBJDEFS in ()
+  with Not_found -> 
+    add_anonymous_object 
+      (inObjDef (o,{o_DEF=c;o_TABS=la;o_TPARAMS=lp;o_TCOMPS=l}))
+;;
+
+
+let ((inObjDef1:section_path -> obj),(outObjDef1:obj -> section_path)) =
+    declare_object ("OBJDEF1",
+                    {load_function = (fun _ -> ());
+                     cache_function = (function  (_,sp) -> ());
+                     specification_function = (function x -> x)});;
+
+
+(* let objdef_info (o1,o2) = 
+  let rec aux = function [] -> raise Not_found 
+                       | (x,y)::l -> if (o1,o2) = x then Left(y)
+                                     else if (o2,o1) = x then Right(y)
+                                          else aux l
+  in aux !oBJDEFS
+;;
+*)
+
+let objdef_info o = assoc o !oBJDEFS;;
+
+let freeze () = !sTRUCS,!oBJDEFS
+;;
+
+let unfreeze (s,o) = sTRUCS:=s;oBJDEFS:=o
+;;
+
+let init () = sTRUCS:=[];oBJDEFS:=[]
+;;
+
+init();;
+
+
+
+Library.declare_summary "objdefs"
+{Summary.freeze_function = freeze;
+ Summary.unfreeze_function = unfreeze;
+ Summary.init_function = init}
+;;
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
new file mode 100755
index 0000000000..d619fd3ae7
--- /dev/null
+++ b/pretyping/recordops.mli
@@ -0,0 +1,48 @@
+
+(* $Id$ *)
+
+(*i*)
+open Names
+open Term
+open Generic
+open Classops
+open Libobject
+open Library
+(*i*)
+
+val nbimpl : int ref
+val nbpathc : int ref
+val nbcoer : int ref
+val nbstruc : int ref
+val nbimplstruc : int ref
+val compter : bool ref
+
+type struc_typ = {
+  s_CONST : identifier; 
+  s_PARAM : int;
+  s_PROJ : section_path option list }
+
+val add_new_struc : Names.section_path * Names.identifier * int *
+    Names.section_path option list -> unit
+val struc_info : Names.section_path -> struc_typ
+
+type obj_typ = {
+  o_DEF : constr;
+  o_TABS : constr list; (* dans l'ordre *)
+  o_TPARAMS : constr list; (* dans l'ordre *)
+  o_TCOMPS : constr list } (* dans l'ordre *)
+               
+val oBJDEFS : ((cte_typ*cte_typ) * obj_typ) list ref
+val sTRUCS : (section_path * struc_typ) list ref
+
+val objdef_info : (cte_typ*cte_typ) -> obj_typ
+val add_new_objdef : (Classops.cte_typ * Classops.cte_typ) * Term.constr * Term.constr list *
+    Term.constr list * Term.constr list -> unit
+
+
+val inStruc : section_path*struc_typ -> obj
+val outStruc : obj -> section_path*struc_typ
+val inObjDef1 : section_path -> obj
+val outObjDef1 : obj -> section_path
+
+val add_new_objdef1 : ((cte_typ*cte_typ) * obj_typ) -> unit