- global_reference traite des variables

 - construct_reference, avec environnement en argument
 - link de Class
 - Definition et Check au toplevel


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

18 files changed, 418 insertions, 349 deletions

diff --git a/.depend b/.depend
index 83d08a63a..96a6e61be 100644
--- a/.depend
+++ b/.depend
@@ -305,6 +305,8 @@ library/declare.cmx: kernel/constant.cmx kernel/environ.cmx kernel/evd.cmx \
     library/libobject.cmx kernel/names.cmx library/nametab.cmx \
     kernel/reduction.cmx kernel/sign.cmx library/summary.cmx kernel/term.cmx \
     kernel/univ.cmx lib/util.cmx library/declare.cmi 
+library/discharge.cmo: library/declare.cmi library/discharge.cmi 
+library/discharge.cmx: library/declare.cmx library/discharge.cmi 
 library/global.cmo: kernel/environ.cmi kernel/generic.cmi \
     kernel/inductive.cmi kernel/instantiate.cmi kernel/safe_typing.cmi \
     kernel/sign.cmi library/summary.cmi kernel/term.cmi lib/util.cmi \
diff --git a/.depend.camlp4 b/.depend.camlp4
index f1671b6ba..21f83048d 100644
--- a/.depend.camlp4
+++ b/.depend.camlp4
@@ -1,27 +1,35 @@
-parsing/g_basevernac.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    toplevel/vernac.cmi 
-parsing/g_basevernac.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
-    toplevel/vernac.cmx 
-parsing/g_command.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi 
-parsing/g_command.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/extend.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/lexer.cmi \
+    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi toplevel/vernac.cmi \
+    parsing/extend.cmi 
+parsing/extend.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/lexer.cmx \
+    parsing/pcoq.cmi lib/pp.cmx lib/util.cmx toplevel/vernac.cmx \
+    parsing/extend.cmi 
+parsing/g_basevernac.cmo: parsing/ast.cmi toplevel/command.cmi \
+    parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
+parsing/g_basevernac.cmx: parsing/ast.cmx toplevel/command.cmx \
+    parsing/coqast.cmx parsing/pcoq.cmi toplevel/vernac.cmx 
+parsing/g_cases.cmo: toplevel/command.cmi parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_cases.cmx: toplevel/command.cmx parsing/coqast.cmx parsing/pcoq.cmi 
+parsing/g_command.cmo: parsing/ast.cmi toplevel/command.cmi \
+    parsing/coqast.cmi parsing/pcoq.cmi 
+parsing/g_command.cmx: parsing/ast.cmx toplevel/command.cmx \
+    parsing/coqast.cmx parsing/pcoq.cmi 
 parsing/g_minicoq.cmo: kernel/generic.cmi parsing/lexer.cmi kernel/names.cmi \
     lib/pp.cmi kernel/sign.cmi kernel/term.cmi kernel/univ.cmi lib/util.cmi \
     parsing/g_minicoq.cmi 
 parsing/g_minicoq.cmx: kernel/generic.cmx parsing/lexer.cmx kernel/names.cmx \
     lib/pp.cmx kernel/sign.cmx kernel/term.cmx kernel/univ.cmx lib/util.cmx \
     parsing/g_minicoq.cmi 
-parsing/g_multiple_case.cmo: parsing/ast.cmi parsing/coqast.cmi \
-    parsing/pcoq.cmi 
-parsing/g_multiple_case.cmx: parsing/ast.cmx parsing/coqast.cmx \
-    parsing/pcoq.cmi 
 parsing/g_prim.cmo: parsing/coqast.cmi parsing/pcoq.cmi 
 parsing/g_prim.cmx: parsing/coqast.cmx parsing/pcoq.cmi 
-parsing/g_tactic.cmo: parsing/ast.cmi parsing/coqast.cmi parsing/pcoq.cmi \
-    lib/pp.cmi 
-parsing/g_tactic.cmx: parsing/ast.cmx parsing/coqast.cmx parsing/pcoq.cmi \
-    lib/pp.cmx 
-parsing/g_vernac.cmo: parsing/coqast.cmi parsing/pcoq.cmi toplevel/vernac.cmi 
-parsing/g_vernac.cmx: parsing/coqast.cmx parsing/pcoq.cmi toplevel/vernac.cmx 
+parsing/g_tactic.cmo: parsing/ast.cmi toplevel/command.cmi parsing/coqast.cmi \
+    parsing/pcoq.cmi lib/pp.cmi lib/util.cmi 
+parsing/g_tactic.cmx: parsing/ast.cmx toplevel/command.cmx parsing/coqast.cmx \
+    parsing/pcoq.cmi lib/pp.cmx lib/util.cmx 
+parsing/g_vernac.cmo: toplevel/command.cmi parsing/coqast.cmi \
+    parsing/pcoq.cmi toplevel/vernac.cmi 
+parsing/g_vernac.cmx: toplevel/command.cmx parsing/coqast.cmx \
+    parsing/pcoq.cmi toplevel/vernac.cmx 
 parsing/pcoq.cmo: parsing/coqast.cmi parsing/lexer.cmi lib/pp.cmi \
     lib/util.cmi parsing/pcoq.cmi 
 parsing/pcoq.cmx: parsing/coqast.cmx parsing/lexer.cmx lib/pp.cmx \
diff --git a/Makefile b/Makefile
index 3cefd6480..e69874b8d 100644
--- a/Makefile
+++ b/Makefile
@@ -75,7 +75,7 @@ TACTICS=tactics/dn.cmo tactics/termdn.cmo tactics/btermdn.cmo \
         tactics/tacentries.cmo tactics/hiddentac.cmo tactics/elim.cmo
 
 TOPLEVEL=toplevel/himsg.cmo toplevel/errors.cmo toplevel/vernacinterp.cmo \
-         toplevel/metasyntax.cmo toplevel/command.cmo pretyping/class.cmo \
+         toplevel/metasyntax.cmo toplevel/command.cmo toplevel/class.cmo \
          toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo
 
@@ -110,8 +110,8 @@ toplevel: $(TOPLEVEL)
 coqtop: $(CMX)
 	$(OCAMLOPT) $(INCLUDES) -o coqtop $(CMXA) $(CMX) $(OSDEPLIBS)
 
-coqtop.byte: $(CMO)
-	ocamlmktop $(INCLUDES) -o coqtop.byte -custom dynlink.cma $(CMA) \
+coqtop.byte: $(CMO) Makefile
+	ocamlmktop $(BYTEFLAGS) -o coqtop.byte -custom dynlink.cma $(CMA) \
 	  $(CMO) $(OSDEPLIBS)
 
 # minicoq
diff --git a/lib/util.ml b/lib/util.ml
index e1e524cf4..b96eca3ae 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -65,6 +65,8 @@ let stringmap_dom m = Stringmap.fold (fun s _ l -> s::l) m []
 
 (* Lists *)
 
+let list_add_set x l = if List.mem x l then l else x::l
+
 let list_intersect l1 l2 = 
   List.filter (fun x -> List.mem x l2) l1
 
diff --git a/lib/util.mli b/lib/util.mli
index 2060b7375..b26d6a1d7 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -41,6 +41,7 @@ val stringmap_dom : 'a Stringmap.t -> string list
 
 (*s Lists. *)
 
+val list_add_set : 'a -> 'a list -> 'a list
 val list_intersect : 'a list -> 'a list -> 'a list
 val list_union : 'a list -> 'a list -> 'a list
 val list_unionq : 'a list -> 'a list -> 'a list
diff --git a/library/declare.ml b/library/declare.ml
index ed63983f7..91fcc7df6 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -218,19 +218,26 @@ let mind_oper_of_id sp id mib =
 	   mip.mind_consnames)
     mib.mind_packets
 
-let global_operator sp id =
+let construct_operator env sp id =
   try
-    let cb = Global.lookup_constant sp in Const sp, cb.const_hyps
+    let cb = Environ.lookup_constant sp env in Const sp, cb.const_hyps
   with Not_found -> 
-    let mib = Global.lookup_mind sp in
+    let mib = Environ.lookup_mind sp env in
     mind_oper_of_id sp id mib, mib.mind_hyps
 
-let global_reference kind id =
+let global_operator sp id = construct_operator (Global.env()) sp id
+
+let construct_reference env kind id =
   let sp = Nametab.sp_of_id kind id in
-  let (oper,_) = global_operator sp id in
-  let hyps = Global.var_context () in
-  let ids = ids_of_sign hyps in
-  DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+  try
+    let (oper,_) = construct_operator env sp id in
+    let hyps = Global.var_context () in
+    let ids = ids_of_sign hyps in
+    DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids))
+  with Not_found -> 
+    VAR (let _ = Environ.lookup_var id env in id)
+
+let global_reference kind id = construct_reference (Global.env()) kind id
 
 let global_reference_imps kind id =
   let c = global_reference kind id in
@@ -241,6 +248,8 @@ let global_reference_imps kind id =
 	c, list_of_implicits (inductive_implicits (sp,i))
     | DOPN (MutConstruct ((sp,i),j),_) ->
 	c, list_of_implicits (constructor_implicits ((sp,i),j))
+    | VAR id ->
+	c, implicits_of_var kind id
     | _ -> assert false
 
 let global env id =
diff --git a/library/declare.mli b/library/declare.mli
index 11f6b2497..4fe7767fd 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -47,17 +47,24 @@ val out_variable : section_path -> identifier * typed_type * strength * bool
 val variable_strength : identifier -> strength
 
 
-(*s It also provides a function [global_reference] to construct a global
-  constr (a constant, an inductive or a constructor) from an identifier.
-  To do so, it first looks for the section path using [Nametab.sp_of_id] and
-  then constructs the corresponding term, associated to the current 
-  environment of variables. *)
+(*s [global_operator sp id] returns the operator (constant, inductive or
+    construtor) corresponding to [(sp,id)] in global environment, together
+    with its definition environment. *)
 
 val global_operator : section_path -> identifier -> sorts oper * var_context
+
+(*s [global_reference k id] returns the object corresponding to
+    the name [id] in the global environment. It may be a constant, 
+    an inductive, a construtor or a variable. It is instanciated
+    on the current environment of variables. [Nametab.sp_of_id] is used
+    to find the corresponding object. 
+    [construct_reference] is a version which looks for variables in a 
+    given environment instead of looking in the current global environment. *)
+
 val global_reference : path_kind -> identifier -> constr
 val global_reference_imps : path_kind -> identifier -> constr * int list
 
-val global : Environ.env -> identifier -> constr
+val construct_reference : Environ.env -> path_kind -> identifier -> constr
 
 val is_global : identifier -> bool
 
diff --git a/parsing/astterm.ml b/parsing/astterm.ml
index e8eb9c3e4..b595c901f 100644
--- a/parsing/astterm.ml
+++ b/parsing/astterm.ml
@@ -148,7 +148,7 @@ let dbize_ref k sigma env loc s =
 	| FW  -> Declare.global_reference_imps FW id
 	| OBJ -> anomaly "search_ref_cci_fw" in
       RRef (loc,ref_from_constr c), il
-    with UserError _ ->
+    with Not_found ->
       try 
 	(Syntax_def.search_syntactic_definition id, [])
       with Not_found -> 
@@ -465,6 +465,16 @@ let fconstr_of_com_env1 is_ass sigma env com =
 let fconstr_of_com_env sigma hyps com =
   fconstr_of_com_env1 false sigma hyps com 
     
+let judgment_of_com1 is_ass sigma env com = 
+  let c = raw_constr_of_com sigma (context env) com in
+  try 
+    ise_resolve is_ass sigma [] env c
+  with e -> 
+    Stdpp.raise_with_loc (Ast.loc com) e
+
+let judgment_of_com sigma env com =
+  judgment_of_com1 false sigma env com
+
 (* Without dB *)
 let type_of_com env com =
   let sign = context env in
diff --git a/parsing/astterm.mli b/parsing/astterm.mli
index 04da5c0e6..8f844e600 100644
--- a/parsing/astterm.mli
+++ b/parsing/astterm.mli
@@ -51,6 +51,10 @@ val fconstr_of_com1 : bool -> 'a evar_map -> env -> Coqast.t -> constr
 val fconstr_of_com : 'a evar_map -> env -> Coqast.t -> constr
 val fconstr_of_com_sort : 'a evar_map -> env -> Coqast.t -> constr
 
+val judgment_of_com1 : 
+  bool -> 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+val judgment_of_com : 'a evar_map -> env -> Coqast.t -> unsafe_judgment
+
 (* Typing with Trad, and re-checking with Mach *)
 (*i
 val fconstruct :'c evar_map -> context -> Coqast.t -> unsafe_judgment
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 97ace7b8a..9816beaa8 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -63,5 +63,4 @@ val ise_resolve_nocheck : 'a evar_map -> (int * constr) list ->
  * Unused outside Trad, but useful for debugging
  *)
 val pretype : 
-  trad_constraint -> env -> 'a evar_defs -> rawconstr 
-    -> unsafe_judgment
+  trad_constraint -> env -> 'a evar_defs -> rawconstr -> unsafe_judgment
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index d619fd3ae..9b666513f 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -22,9 +22,9 @@ type struc_typ = {
   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
+val add_new_struc : 
+  section_path * identifier * int * section_path option list -> unit
+val struc_info : section_path -> struc_typ
 
 type obj_typ = {
   o_DEF : constr;
@@ -32,17 +32,18 @@ type obj_typ = {
   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 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 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 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
+val add_new_objdef1 : ((cte_typ * cte_typ) * obj_typ) -> unit
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index 926e2601c..ce9ea7390 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -19,10 +19,9 @@ val get_type_of_with_meta : env -> 'a evar_map -> metamap -> constr -> constr
 val get_sort_of : env -> 'a evar_map -> constr -> sorts
 
 (*i The following should be merged with mind_specif and put elsewhere 
-    Note : it needs Reduction
-i*)
+    Note : it needs Reduction i*)
 
-(* A light version of mind_specif *)
+(* A light version of [mind_specif] *)
 
 (* Invariant: We have\\
    -- Hnf (fullmind) = DOPN(AppL,[|coremind;..params..;..realargs..|])\\
@@ -30,14 +29,14 @@ i*)
  *)
 type mutind_id = inductive_path * constr array
 
-type mutind =
-    {fullmind : constr;
-     mind : mutind_id;
-     nparams : int;
-     nconstr : int;
-     params : constr list;
-     realargs : constr list;
-     arity : constr};;
+type mutind = {
+  fullmind : constr;
+  mind : mutind_id;
+  nparams : int;
+  nconstr : int;
+  params : constr list;
+  realargs : constr list;
+  arity : constr }
 
 (* [try_mutind_of sigma t] raise Induc if [t] is not an inductive type *)
 val try_mutind_of : env -> 'a Evd.evar_map -> constr -> mutind
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 49315aba7..446d70b43 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -78,7 +78,7 @@ let pf_constr_of_com_sort gls c =
   let evc = project gls in 
   Astterm.constr_of_com_sort evc (sig_it gls).evar_env c
 
-let pf_global gls id = Declare.global (sig_it gls).evar_env id
+let pf_global gls id = Declare.construct_reference (sig_it gls).evar_env CCI id
 let pf_parse_const gls = compose (pf_global gls) id_of_string
 
 let pf_execute gls =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 18902c7b3..5f4c73fea 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1678,7 +1678,7 @@ let abstract_subproof name tac gls =
     with UserError _ as e -> 
       (abort_cur_goal(); raise e)
   end;
-  exact (applist ((Declare.global env' na), 
+  exact (applist ((Declare.construct_reference env' CCI na), 
                   (List.map (fun id -> VAR(id)) 
                      (List.rev (ids_of_sign sign)))))
     gls
diff --git a/toplevel/class.ml b/toplevel/class.ml
index 5c762636f..dbd088555 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -1,4 +1,6 @@
 
+(* $Id$ *)
+
 open Util
 open Pp
 open Names
@@ -18,7 +20,7 @@ open Declare
 (* strength * strength -> bool *)
 
 let stre_gt = function
-    (NeverDischarge,NeverDischarge) -> false
+  | (NeverDischarge,NeverDischarge) -> false
   | (NeverDischarge,x) -> false
   | (x,NeverDischarge) -> true
   | (DischargeAt sp1,DischargeAt sp2) -> sp_gt (sp1,sp2) 
@@ -30,7 +32,7 @@ let stre_max4 stre1 stre2 stre3 stre4 =
   stre_max ((stre_max (stre1,stre2)),(stre_max (stre3,stre4)))
 
 let id_of_varid = function
-  | (VAR id) -> id
+  | VAR id -> id
   | _ -> anomaly "class__id_of_varid"
 
 let stre_of_VAR c = variable_strength (destVar c)
@@ -39,24 +41,25 @@ let stre_of_VAR c = variable_strength (destVar c)
    lc liste des variable dont depend la classe source *)
 
 let rec stre_unif_cond = function
-    ([],[]) -> NeverDischarge
+  | ([],[]) -> NeverDischarge
   | (v::l,[]) -> stre_of_VAR v
   | ([],v::l) -> stre_of_VAR v
   | (v1::l1,v2::l2) ->
-      if v1=v2 then stre_unif_cond (l1,l2)
+      if v1=v2 then 
+	stre_unif_cond (l1,l2)
       else
 	let stre1 = (stre_of_VAR v1)
-	and stre2 = (stre_of_VAR v2)
-	in stre_max (stre1,stre2)
+	and stre2 = (stre_of_VAR v2) in 
+	stre_max (stre1,stre2)
 
 let stre_of_coe = function
-    NAM_SP sp ->
+  | NAM_SP sp ->
       (match global_operator sp (basename sp) with
-	   Const sp, _ -> constant_strength sp
+	 | Const sp, _ -> constant_strength sp
 	 | _ -> NeverDischarge)
   | NAM_Var id -> variable_strength id
   | _ -> NeverDischarge
-
+	
 (* try_add_class : Names.identifier ->
   Term.constr -> (cl_typ * int) option -> bool -> int * Libobject.strength *)
 
@@ -64,24 +67,28 @@ let try_add_class id v clpopt streopt check_exist =
   let env = Global.env () in
   let t = Retyping.get_type_of env Evd.empty v in
   let p1 =
-    try arity_sort t 
-    with Not_found -> errorlabstrm "try_add_class" 
+    try 
+      arity_sort t 
+    with Not_found -> 
+      errorlabstrm "try_add_class" 
         [< 'sTR "Type of "; 'sTR (string_of_id id);
-           'sTR " does not end with a sort" >] in
+           'sTR " does not end with a sort" >] 
+  in
   let cl,p =
     match clpopt with
-        None -> let (cl,_)=constructor_at_head v in (cl,p1)
-      | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) in
+      | None -> let (cl,_)=constructor_at_head v in (cl,p1)
+      | Some (cl,p2) -> (fully_applied id p2 p1;cl,p1) 
+  in
   if check_exist & class_exists cl then
     errorlabstrm "try_add_new_class" 
       [< 'sTR (string_of_id id) ; 'sTR " is already a class" >];
   let stre' = stre_of_cl cl in 
-  let stre = (match streopt with
-                  (Some stre) -> stre_max (stre,stre')
-                | None -> stre') in
-    add_new_class (cl,(string_of_id id),stre,p);
-    stre
-
+  let stre = match streopt with
+    | Some stre -> stre_max (stre,stre')
+    | None -> stre'
+  in
+  add_new_class (cl,(string_of_id id),stre,p);
+  stre
 
 (* try_add_new_class : Names.identifier -> unit *)
 
@@ -89,18 +96,19 @@ let try_add_new_class id stre =
   let v = global_reference CCI id in
   let _ = try_add_class id v None (Some stre) true in () 
 
-
 (* check_class : Names.identifier ->
   Term.constr -> cl_typ -> int -> int * Libobject.strength *)
 
 let check_class id v cl p =
- try 
-   let _,clinfo = class_info cl in
-   if p = clinfo.cL_PARAM
-   then clinfo.cL_STRE
-   else errorlabstrm "fully_applied" 
-     [< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
- with Not_found -> try_add_class id v (Some (cl,p)) None false
+  try 
+    let _,clinfo = class_info cl in
+    if p = clinfo.cL_PARAM then 
+      clinfo.cL_STRE
+    else 
+      errorlabstrm "fully_applied" 
+	[< 'sTR"Wrong number of parameters for ";'sTR(string_of_id id) >]
+  with Not_found -> 
+    try_add_class id v (Some (cl,p)) None false
 
 
 (* decomposition de constr vers coe_typ *)
@@ -108,48 +116,52 @@ let check_class id v cl p =
 let coe_constructor_at_head t = 
   let rec aux t' =
     match kind_of_term t' with
-    IsConst (sp,l) -> (Array.to_list l),NAM_SP sp
-  | IsMutInd (sp,_,l) -> (Array.to_list l),NAM_SP sp
-  | IsVar id  -> [],NAM_Var id
-  | IsCast (c,_) -> aux c
-  | IsMutConstruct (sp,i,j,l) -> (Array.to_list l),NAM_Construct ((sp,i),j)
-  | IsAppL(f,args) -> aux f
-  |  _ -> raise Not_found
-  in aux (collapse_appl t)
+      | IsConst (sp,l) -> (Array.to_list l),NAM_SP sp
+      | IsMutInd (sp,_,l) -> (Array.to_list l),NAM_SP sp
+      | IsVar id  -> [],NAM_Var id
+      | IsCast (c,_) -> aux c
+      | IsMutConstruct (sp,i,j,l) -> (Array.to_list l),NAM_Construct ((sp,i),j)
+      | IsAppL(f,args) -> aux f
+      |  _ -> raise Not_found
+  in 
+  aux (collapse_appl t)
 
 let constructor_at_head1 t = 
   let rec aux t' =
     match kind_of_term t' with
-    IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0
-  | IsMutInd (sp,i,l) -> t',[],(Array.to_list l),CL_IND (sp,i),0
-  | IsVar id -> t',[],[],CL_Var id,0
-  | IsCast (c,_) -> aux c
-  | IsAppL(f,args) -> let t',_,l,c,_ = aux f in t',args,l,c,List.length args
-  | IsProd (_,_,_) -> t',[],[],CL_FUN,0
-  | IsSort _ -> t',[],[],CL_SORT,0
-  |  _ -> raise Not_found
-  in aux (collapse_appl t)
+      | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0
+      | IsMutInd (sp,i,l) -> t',[],(Array.to_list l),CL_IND (sp,i),0
+      | IsVar id -> t',[],[],CL_Var id,0
+      | IsCast (c,_) -> aux c
+      | IsAppL(f,args) -> 
+	  let t',_,l,c,_ = aux f in t',args,l,c,List.length args
+      | IsProd (_,_,_) -> t',[],[],CL_FUN,0
+      | IsSort _ -> t',[],[],CL_SORT,0
+      |  _ -> raise Not_found
+  in 
+  aux (collapse_appl t)
 
 
 (* condition d'heritage uniforme *)
 
 let uniform_cond nargs lt = 
   let rec aux = function
-      (0,[]) -> true
+    | (0,[]) -> true
     | (n,t::l) -> (strip_outer_cast t = Rel n) & (aux ((n-1),l))
     | _ -> false
-  in aux (nargs,lt)
+  in 
+  aux (nargs,lt)
 
 let id_of_cl  = function
-    CL_FUN -> (id_of_string "FUNCLASS")
+  | CL_FUN -> (id_of_string "FUNCLASS")
   | CL_SORT -> (id_of_string "SORTCLASS") 
   | CL_SP sp -> (basename sp)
   | CL_IND (sp,i) ->
       (mind_nth_type_packet (Global.lookup_mind sp) i).mind_typename
   | CL_Var id -> id 
-
+	
 let string_of_cl  = function
-    CL_FUN -> "FUNCLASS"
+  | CL_FUN -> "FUNCLASS"
   | CL_SORT -> "SORTCLASS" 
   | CL_SP sp -> string_of_id (basename sp)
   | CL_IND (sp,i) ->
@@ -174,95 +186,112 @@ type choice = Ident of identifier | Section_path of section_path
 let get_source lp source =
   let aux test =
     let rec aux1 n = function
-	[] -> raise Not_found
+      | [] -> raise Not_found
       | t1::lt ->
-	  try (let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
-               if test cl1
-               then cl1,p1,v1,lv1,n,l
-               else aux1 (n+1) lt)
-          with _ -> aux1 (n + 1) lt
-    in aux1 1 lp
-  in match source with
-      None ->
+	  try 
+	    let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
+            if test cl1 then 
+	      cl1,p1,v1,lv1,n,l
+            else 
+	      aux1 (n+1) lt
+          with _ -> 
+	    aux1 (n + 1) lt
+    in 
+    aux1 1 lp
+  in 
+  match source with
+    | None ->
 	let (v1,lv1,l,cl1,p1) as x =
-	  (match lp with
-	       [] -> raise Not_found
-             | t1::_ ->
-		 try constructor_at_head1 t1
-                 with _ -> raise Not_found)
-        in (id_of_cl cl1),(cl1,p1,v1,lv1,1,l)
-    | Some (Ident id) -> id, aux (function cl -> id_of_cl cl = id)
+	  match lp with
+	    | [] -> raise Not_found
+            | t1::_ ->
+		try constructor_at_head1 t1
+                with _ -> raise Not_found
+        in 
+	(id_of_cl cl1),(cl1,p1,v1,lv1,1,l)
+    | Some (Ident id) -> 
+	id, aux (function cl -> id_of_cl cl = id)
     | Some (Section_path sp) ->
 	basename sp,
 	aux (function
-		 CL_SP sp1 -> sp=sp1
+	       | CL_SP sp1 -> sp=sp1
 	       | CL_IND (sp1,i) -> sp=sp1
                | _ -> false)
 
 let get_target t ind =
- if (ind > 1) 
- then CL_FUN,0,t
- else let v2,_,_,cl2,p2 = constructor_at_head1 t in
-       cl2,p2,v2
-
+  if (ind > 1) then 
+    CL_FUN,0,t
+  else 
+    let v2,_,_,cl2,p2 = constructor_at_head1 t in cl2,p2,v2
 
 let prods_of t = 
   let rec aux acc = function
-      DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2
+    | DOP2(Prod,c1,DLAM(_,c2)) -> aux (c1::acc) c2
     | (DOP2(Cast,c,_)) -> aux acc c
     | t -> t::acc
-  in aux [] t
+  in 
+  aux [] t
 
 (* coercion identite' *)
 
 let lams_of t = 
   let rec aux acc = function
-      DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2
-    | (DOP2(Cast,c,_)) -> aux acc c
+    | DOP2(Lambda,c1,DLAM(x,c2)) -> aux ((x,c1)::acc) c2
+    | DOP2(Cast,c,_) -> aux acc c
     | t -> acc,t
-  in aux [] t
+  in 
+  aux [] t
 
 let build_id_coercion idf_opt ids =
   let env = Global.env () in
-  let vs = global env ids in 
+  let vs = construct_reference env CCI ids in 
   let c = match (strip_outer_cast vs) with
-      (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' ->
+    | (DOPN(Const sp,l) as c') when Environ.evaluable_constant env c' ->
 	(try Instantiate.constant_value env c'
          with _ -> errorlabstrm "build_id_coercion"
              [< 'sTR(string_of_id ids);
 		'sTR" must be a transparent constant" >])
-    | _ -> errorlabstrm "build_id_coercion"
-        [< 'sTR(string_of_id ids); 'sTR" must be a transparent constant" >] in
+    | _ -> 
+	errorlabstrm "build_id_coercion"
+          [< 'sTR(string_of_id ids); 
+	     'sTR" must be a transparent constant" >] 
+  in
   let lams,t = lams_of c in
   let lams = List.rev lams in
   let llams = List.length lams in
   let val_f =
     List.fold_right
-      (fun (x,t) u ->
-	 DOP2(Lambda,t,DLAM(x,u)))
+      (fun (x,t) u -> DOP2(Lambda,t,DLAM(x,u)))
       lams
       (DOP2(Lambda,(applistc vs (rel_list 0 llams)),
-	    DLAM(Name (id_of_string "x"),Rel 1))) in
+	    DLAM(Name (id_of_string "x"),Rel 1))) 
+  in
   let typ_f =
     List.fold_right
       (fun (x,t) c -> DOP2(Prod,t,DLAM(x,c)))
       lams
       (DOP2(Prod,(applistc vs (rel_list 0 llams)),
-	    DLAM(Anonymous,lift 1 t))) in 
+	    DLAM(Anonymous,lift 1 t))) 
+  in 
   let constr_f = DOP2(Cast,val_f,typ_f) in
   (* juste pour verification *)
-  let _ = try Typing.type_of env Evd.empty constr_f
-  with _ -> 
-    error "cannot be defined as coercion - may be a bad number of arguments" in
+  let _ = 
+    try 
+      Typing.type_of env Evd.empty constr_f
+    with _ -> 
+      error ("cannot be defined as coercion - "^
+	     "may be a bad number of arguments") 
+  in
   let idf =
-    (match idf_opt with
-	 Some(idf) -> idf
-       | None ->
-	   id_of_string ("Id_"^(string_of_id ids)^"_"^
-                         (string_of_cl (fst (constructor_at_head t))))) in
+    match idf_opt with
+      | Some(idf) -> idf
+      | None ->
+	  id_of_string ("Id_"^(string_of_id ids)^"_"^
+                        (string_of_cl (fst (constructor_at_head t)))) 
+  in
   let constr_entry = {const_entry_body = constr_f; const_entry_type = None } in
-  let _ = declare_constant idf (constr_entry,NeverDischarge,false)
-  in idf
+  declare_constant idf (constr_entry,NeverDischarge,false);
+  idf
 
 let coercion_syntax_entry id n =
   let args = (String.concat " " (list_tabulate (fun _ -> "$_") n)) ^ " $c" in
@@ -270,41 +299,41 @@ let coercion_syntax_entry id n =
             " [ <<(" ^ (string_of_id id) ^ " " ^ args ^ ")>> ]" ^
             " -> [ (APPLIST $c):E ]"
   in
-    try
-      let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
-        Metasyntax.add_syntax_obj "constr" [se]
-    with Stdpp.Exc_located _ -> anomaly ("ill-formed syntax entry: "^str)
+  try
+    let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
+    Metasyntax.add_syntax_obj "constr" [se]
+  with Stdpp.Exc_located _ -> 
+    anomaly ("ill-formed syntax entry: "^str)
 
 let fun_coercion_syntax_entry id n =
   let args =
-    if n<0 then anomaly "fun_coercion_syntax_entry"
-    else
-      String.concat " " (list_tabulate (fun _ -> "$_") n) ^ " $c ($LIST $l)" in
+    if n<0 then anomaly "fun_coercion_syntax_entry";
+    String.concat " " (list_tabulate (fun _ -> "$_") n) ^ " $c ($LIST $l)" 
+  in
   let str = "level 10: " ^ ((string_of_id id)^"1") ^
             " [ (APPLIST " ^ (string_of_id id) ^ " " ^ args ^ ") ] "  ^
       	    "-> [ (APPLIST $c ($LIST $l)):E ]"
   in
-    try
-      let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
-        Metasyntax.add_syntax_obj "constr" [se]
-    with Stdpp.Exc_located _ -> anomaly ("ill-formed syntax entry: "^str)
-
-
+  try
+    let se = Pcoq.parse_string Pcoq.Prim.syntax_entry_eoi str in
+    Metasyntax.add_syntax_obj "constr" [se]
+  with Stdpp.Exc_located _ -> 
+    anomaly ("ill-formed syntax entry: "^str)
 
 let coercion_syntax idf ps clt =
   match clt with
-      CL_FUN -> 
-	(fun_coercion_syntax_entry idf ps;
-	 coercion_syntax_entry idf ps)
+    | CL_FUN -> 
+	fun_coercion_syntax_entry idf ps;
+	coercion_syntax_entry idf ps
     | _ -> coercion_syntax_entry idf ps
 
-
 let add_new_coercion_in_graph1 (coef,v,stre,isid,cls,clt) idf ps =
   let _ = add_anonymous_leaf
-    (inCoercion
-       ((coef,
-	 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
-	cls,clt)) in
+	    (inCoercion
+	       ((coef,
+		 {cOE_VALUE=v;cOE_STRE=stre;cOE_ISID=isid;cOE_PARAM=ps}),
+		cls,clt)) 
+  in
   coercion_syntax idf ps clt
 
 (* 
@@ -320,28 +349,29 @@ lorque source est None alors target est None aussi.
 
 let try_add_new_coercion_core idf stre source target isid =
   let env = Global.env () in
-  let v = global env idf in
+  let v = construct_reference env CCI idf in
   let t = Retyping.get_type_of env Evd.empty v in
   let k = Retyping.get_type_of env Evd.empty t in
   let vj = {uj_val=v; uj_type=t; uj_kind = k} in
   let f_vardep,coef = coe_constructor_at_head v in
   if coercion_exists coef then
-      errorlabstrm "try_add_coercion" 
-	[< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
+    errorlabstrm "try_add_coercion" 
+      [< 'sTR(string_of_id idf) ; 'sTR" is already a coercion" >];
   let lp = prods_of t in
   let llp = List.length lp in
   if llp <= 1 then
     errorlabstrm "try_add_coercion"         
       [< 'sTR"Does not correspond to a coercion" >];
-
   let ids,(cls,ps,vs,lvs,ind,s_vardep) =
-    try get_source (List.tl lp) source
-    with Not_found -> errorlabstrm "try_add_coercion" 
-        [<'sTR"We do not find the source class " >] in
-
+    try 
+      get_source (List.tl lp) source
+    with Not_found -> 
+      errorlabstrm "try_add_coercion" 
+        [<'sTR"We do not find the source class " >] 
+  in
   if (cls = CL_FUN) then
     errorlabstrm "try_add_coercion" 
-              [< 'sTR"FUNCLASS cannot be a source class" >];
+      [< 'sTR"FUNCLASS cannot be a source class" >];
   if (cls = CL_SORT) then
     errorlabstrm "try_add_coercion" 
       [< 'sTR"SORTCLASS cannot be a source class" >];
@@ -349,19 +379,24 @@ let try_add_new_coercion_core idf stre source target isid =
     errorlabstrm "try_add_coercion" 
       [<'sTR(string_of_id idf);
         'sTR" does not respect the inheritance uniform condition" >];
-
   let clt,pt,vt =
-    try get_target (List.hd lp) ind 
-    with Not_found -> errorlabstrm "try_add_coercion" 
-        [<'sTR"We cannot find the target class" >] in
+    try 
+      get_target (List.hd lp) ind 
+    with Not_found -> 
+      errorlabstrm "try_add_coercion" 
+        [<'sTR"We cannot find the target class" >] 
+  in
   let idt =
     (match target with
-	 Some idt -> 
-	   if idt = id_of_cl clt then idt
-	   else errorlabstrm "try_add_coercion" 
-             [<'sTR"The target class does not correspond to ";
-	       'sTR(string_of_id idt) >]
-       | None -> (id_of_cl clt)) in
+       | Some idt -> 
+	   if idt = id_of_cl clt then 
+	     idt
+	   else 
+	     errorlabstrm "try_add_coercion" 
+               [<'sTR"The target class does not correspond to ";
+		 'sTR(string_of_id idt) >]
+       | None -> (id_of_cl clt)) 
+  in
   let stres = check_class ids vs cls ps in
   let stret = check_class idt vt clt pt in
   let stref = stre_of_coe coef in
@@ -403,44 +438,46 @@ let defined_in_sec sp sec_sp =
 let process_class sec_sp ((cl,{cL_STR=s;cL_STRE=stre;cL_PARAM=p}) as x ) =
   let env = Global.env () in
   match cl with 
-      CL_Var id -> x
+    | CL_Var id -> x
     | CL_SP sp -> 
-        if defined_in_sec sp sec_sp 
-        then
+        if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
           let newsp = Lib.make_path spid CCI in 
           let v = global_reference CCI spid in
           let t = Retyping.get_type_of env Evd.empty v in
           let p = arity_sort t in
           (CL_SP newsp,{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
-        else x
+        else 
+	  x
     | CL_IND (sp,i) ->
-        if defined_in_sec sp sec_sp 
-        then
+        if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
           let newsp = Lib.make_path spid CCI in 
           let v = global_reference CCI spid in
           let t = Retyping.get_type_of env Evd.empty v in
           let p = arity_sort t in
           (CL_IND (newsp,i),{cL_STR=s;cL_STRE=stre;cL_PARAM=p})
-        else x
+        else 
+	  x
     | _ -> anomaly "process_class" 
 
 let process_cl sec_sp cl =
   match cl with
-      CL_Var id -> CL_Var id 
+    | CL_Var id -> CL_Var id 
     | CL_SP sp ->
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
           let newsp = Lib.make_path spid CCI in 
           CL_SP newsp
-        else cl
+        else 
+	  cl
     | CL_IND (sp,i) ->
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
           let newsp = Lib.make_path spid CCI in 
           CL_IND (newsp,i)
-        else cl
+        else 
+	  cl
     | _ -> cl
 
 let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
@@ -448,14 +485,15 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
   let t1 = process_cl sec_sp t in
   let p = (snd (class_info s1)).cL_PARAM in
   match coe with 
-      NAM_Var id -> ((coe,coeinfo),s1,t1),id,p
+    | NAM_Var id -> ((coe,coeinfo),s1,t1),id,p
     | NAM_SP sp -> 
 	if defined_in_sec sp sec_sp then
 	  let ((_,spid,spk)) = repr_path sp in
 	  let newsp = Lib.make_path spid CCI in
 	  let v = global_reference CCI spid in
 	  ((NAM_SP newsp,coeinfo),s1,t1),spid,p
-	else ((coe,coeinfo),s1,t1),basename sp,p
+	else 
+	  ((coe,coeinfo),s1,t1),basename sp,p
     | NAM_Construct ((sp,i),j) -> 
 	if defined_in_sec sp sec_sp then 
 	  let ((_,spid,spk)) = repr_path sp in
@@ -467,5 +505,3 @@ let process_coercion sec_sp (((coe,coeinfo),s,t) as x) =
 	  ((coe,coeinfo),s1,t1),
 	  Global.id_of_global (MutConstruct((sp,i),j)),
 	  p
-
-(* Id: class.ml4,v 1.2 1997/06/17 17:44:10 dderaugl Exp $ *)
diff --git a/toplevel/record.ml b/toplevel/record.ml
index cc44bc22b..99cbac0b8 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -1,80 +1,72 @@
 
 (* $:Id$ *)
 
-open Util;;
-open Names;;
-open Term;;
+open Pp
+open Util
+open Names
+open Term
+open Coqast
+open Ast
 (*
-open Generic;;
-open Mach;;
-open Command;;
-open More_util;;
-open Pp;;
-
-open Constrtypes;;
-open Termenv;;
-open Trad;;
-open Ast;;
-open CoqAst;;
-
-open Machops;;
-open Classops;;
-open Recordops;;
+open Generic
+open Command
+open Machops
+open Classops
+open Recordops
 *)
 
 (********** definition d'un record (structure) **************)
 
 let make_constructor fields appc =
- let rec aux fields =
-  match fields with
-     [] -> appc
-   | (id,ty)::l -> ope("PROD",[ty; slam(Some (string_of_id id), aux l)]) 
- in aux fields;;
+  let rec aux fields =
+    match fields with
+      | [] -> appc
+      | (id,ty)::l -> ope("PROD",[ty; slam(Some (string_of_id id), aux l)]) 
+  in 
+  aux fields
 
 (* free_vars existe de'ja` dans ast.ml *)
 
 let rec drop = function
-    [] -> []
+  | [] -> []
   | (None::t) -> drop t
   | ((Some id)::t) -> id::(drop t)
-;;
 
 let fold curriedf l base =
   List.fold_right (fun a -> fun b -> curriedf(a,b)) l base
-;;
-
+    
 let free_vars t = 
- let rec aux = function
-  (Nvar(_,s),accum) -> add_set (id_of_string s) accum
-| (Node(_,_,tl),accum) -> fold aux tl accum
-| (Slam(_,None,body),accum) ->
-        (aux(body,[]))@accum
-| (Slam(_,Some id,body),accum) ->
-        (subtract (aux(body,[])) [(id_of_string id)])@accum
-| (_,accum) -> accum
- in aux(t,[]) 
-;;
+  let rec aux = function
+    | (Nvar(_,s),accum) -> list_add_set (id_of_string s) accum
+    | (Node(_,_,tl),accum) -> fold aux tl accum
+    | (Slam(_,None,body),accum) -> (aux(body,[]))@accum
+    | (Slam(_,Some id,body),accum) ->
+	(list_subtract (aux(body,[])) [(id_of_string id)])@accum
+    | (_,accum) -> accum
+  in 
+  aux(t,[]) 
 
 let free_in_asts id l = 
   let rec aux =
-    function [] -> true
-      | a::l -> (not (List.mem id (free_vars a))) & (aux l) in
-  aux l;;
+    function 
+      | [] -> true
+      | a::l -> (not (List.mem id (free_vars a))) & (aux l) 
+  in
+  aux l
 
 let all_vars t = 
- let rec aux = function
-  (Nvar(_,id),accum) -> add_set (id_of_string id) accum
-| (Node(_,_,tl),accum) -> fold aux tl accum
-| (Slam(_,None,body),accum) -> aux (body,accum)
-| (Slam(_,Some id,body),accum) ->
-    aux (body,(union accum [(id_of_string id)]))
-| (_,accum) -> accum
- in aux(t,[]) 
-;;
+  let rec aux = function
+    | (Nvar(_,id),accum) -> list_add_set (id_of_string id) accum
+    | (Node(_,_,tl),accum) -> fold aux tl accum
+    | (Slam(_,None,body),accum) -> aux (body,accum)
+    | (Slam(_,Some id,body),accum) ->
+	aux (body,(list_union accum [(id_of_string id)]))
+    | (_,accum) -> accum
+  in 
+  aux(t,[]) 
    
 let print_id_list l =
   [< 'sTR "[" ; prlist (fun id -> [< 'sTR (string_of_id id) >]) l; 'sTR "]" >]
-;; 
 
 let typecheck_params_and_field ps fs =
   let sign0 = initial_sign() in
@@ -82,89 +74,89 @@ let typecheck_params_and_field ps fs =
     List.fold_left
       (fun (sign,newps) (id,t) -> 
          let tj = type_of_com sign t in
-           (add_sign (id,tj) sign,(id,tj.body)::newps))
-      (sign0,[]) ps in
+         (add_sign (id,tj) sign,(id,tj.body)::newps))
+      (sign0,[]) ps 
+  in
   let sign2,newfs =
     List.fold_left
       (fun (sign,newfs) (id,t) -> 
          let tj = type_of_com sign t in
-           (add_sign (id,tj) sign,(id,tj.body)::newfs)) (sign1,[]) fs
-  in List.rev(newps),List.rev(newfs)
-;;
-
-
-let mk_LambdaCit = List.fold_right (fun (x,a) b -> mkNamedLambda x a b);;
+         (add_sign (id,tj) sign,(id,tj.body)::newfs)) (sign1,[]) fs
+  in
+  List.rev(newps),List.rev(newfs)
 
+let mk_LambdaCit = List.fold_right (fun (x,a) b -> mkNamedLambda x a b)
 
 let definition_structure (coe_constr,struc,ps,cfs,const,s) =
-
- let (sign,fsign) = initial_assumptions() in
- let fs = List.map snd cfs in     
- let coers = List.map fst cfs in  
- let idps = List.map fst ps in      
- let typs = List.map snd ps in
- let idfs = List.map fst fs in
- let tyfs = List.map snd fs in
- let _ = if not (free_in_asts struc tyfs)
-            then message "Error: A record cannot be recursive" in
- let newps,newfs = typecheck_params_and_field ps fs in
- let app_constructor = ope("APPLIST",
-                           (ope("XTRA",[str "!";(nvar (string_of_id struc))]))::
-                           List.map (fun id -> nvar(string_of_id id)) idps) in
- let type_constructor = make_constructor fs app_constructor in 
- let _ = build_mutual ps [(struc,s,[(const,type_constructor)])] true in
-
- let x = next_ident_away (id_of_string "x") 
-               (List.fold_left (fun l ty -> union (all_vars ty) l) 
+  let (sign,fsign) = initial_assumptions() in
+  let fs = List.map snd cfs in     
+  let coers = List.map fst cfs in  
+  let idps = List.map fst ps in      
+  let typs = List.map snd ps in
+  let idfs = List.map fst fs in
+  let tyfs = List.map snd fs in
+  if not (free_in_asts struc tyfs) then 
+    message "Error: A record cannot be recursive";
+  let newps,newfs = typecheck_params_and_field ps fs in
+  let app_constructor = 
+    ope("APPLIST",
+        (ope("XTRA",[str "!";(nvar (string_of_id struc))]))::
+        List.map (fun id -> nvar(string_of_id id)) idps) 
+  in
+  let type_constructor = make_constructor fs app_constructor in 
+  let _ = build_mutual ps [(struc,s,[(const,type_constructor)])] true in
+  let x = next_ident_away (id_of_string "x") 
+            (List.fold_left (fun l ty -> union (all_vars ty) l) 
                (union idps (fst sign)) tyfs) in
- let r = Machops.global (gLOB sign) struc in
- let (rsp,_,_) = destMutInd r in
- let rid = basename rsp in
- let lp = length idps in
- let rp1 = applist (r,(rel_list 0 lp)) in
- let rp2 = applist (r,(rel_list 1 lp)) in
- let warning_or_error coe st = if coe then (errorlabstrm "structure" st)
-                               else pPNL [< 'sTR"Warning: "; st >] in
-        
- let (sp_projs,_,_,_,_) =
-   List.fold_left 
-   (fun (sp_projs,ids_ok,ids_not_ok,sigma,coes) (fi,ti) -> 
-      let fv_ti = global_vars ti in
-      let bad_projs = (intersect ids_not_ok fv_ti) in
-      if bad_projs <> []
-      then begin (warning_or_error (hd coes)
-                   [< 'sTR(string_of_id fi); 
-                      'sTR" cannot be defined. The projections ";
-                         print_id_list bad_projs; 'sTR " were not defined" >]);
-                 (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes))
-           end
-      else 
-
-      let p = mkNamedLambda x rp2 (replace_vars sigma ti) in
-      let branch = mk_LambdaCit newfs (VAR fi) in
-      let proj = mk_LambdaCit newps 
-             (mkNamedLambda x rp1 (mkMutCaseA (ci_of_mind r) p (Rel 1) [|branch|])) in
-      let ok = try (Declare.machine_constant (sign,fsign)
-                    ((fi,false,NeverDischarge),proj); true)
-               with UserError(s,pps) ->
-                 ((warning_or_error (hd coes) 
-                     [<'sTR (string_of_id fi); 
-                       'sTR" cannot be defined. "; pps >]);false) in
-      if not ok
-      then (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes))
-      else begin
-        if List.hd coes then
-           Class.try_add_new_coercion_record fi NeverDischarge rsp;
-        let constr_fi = Machops.global (gLOB sign) fi in
-        let constr_fip =
-          applist (constr_fi,(List.map (fun id -> VAR id) idps)@[VAR x])
-        in (Some(path_of_const constr_fi)::sp_projs,fi::ids_ok,ids_not_ok,
-            (fi,{sinfo=Closed;sit=constr_fip})::sigma,(tl coes))
-      end)
-     ([],[],[],[],coers) newfs
-   in (if coe_constr="COERCION" 
-     then Class.try_add_new_coercion const NeverDischarge);
-          add_new_struc (rsp,const,lp,rev sp_projs)
-;;
-         
-(* $Id$ *)
+  let r = Machops.global (gLOB sign) struc in
+  let (rsp,_,_) = destMutInd r in
+  let rid = basename rsp in
+  let lp = length idps in
+  let rp1 = applist (r,(rel_list 0 lp)) in
+  let rp2 = applist (r,(rel_list 1 lp)) in
+  let warning_or_error coe st = 
+    if coe then errorlabstrm "structure" st;
+    pPNL [< 'sTR"Warning: "; st >] 
+  in
+  let (sp_projs,_,_,_,_) =
+    List.fold_left 
+      (fun (sp_projs,ids_ok,ids_not_ok,sigma,coes) (fi,ti) -> 
+	 let fv_ti = global_vars ti in
+	 let bad_projs = (intersect ids_not_ok fv_ti) in
+	 if bad_projs <> [] then begin 
+	   (warning_or_error (hd coes)
+              [< 'sTR(string_of_id fi); 
+		 'sTR" cannot be defined. The projections ";
+                 print_id_list bad_projs; 'sTR " were not defined" >]);
+           (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes))
+         end else 
+	   let p = mkNamedLambda x rp2 (replace_vars sigma ti) in
+	   let branch = mk_LambdaCit newfs (VAR fi) in
+	   let proj = mk_LambdaCit newps 
+			(mkNamedLambda x rp1 
+			   (mkMutCaseA (ci_of_mind r) p (Rel 1) [|branch|])) in
+	   let ok = 
+	     try 
+	       (Declare.machine_constant (sign,fsign)
+		  ((fi,false,NeverDischarge),proj); true)
+             with UserError(s,pps) ->
+               ((warning_or_error (hd coes) 
+                   [<'sTR (string_of_id fi); 
+                     'sTR" cannot be defined. "; pps >]);false) in
+	   if not ok then 
+	     (None::sp_projs,ids_ok,fi::ids_not_ok,sigma,(tl coes))
+	   else begin
+             if List.hd coes then
+               Class.try_add_new_coercion_record fi NeverDischarge rsp;
+             let constr_fi = Machops.global (gLOB sign) fi in
+             let constr_fip =
+               applist (constr_fi,(List.map (fun id -> VAR id) idps)@[VAR x])
+             in (Some(path_of_const constr_fi)::sp_projs,fi::ids_ok,ids_not_ok,
+		 (fi,{sinfo=Closed;sit=constr_fip})::sigma,(tl coes))
+	   end)
+      ([],[],[],[],coers) newfs
+  in 
+  if coe_constr="COERCION" then 
+    Class.try_add_new_coercion const NeverDischarge;
+  add_new_struc (rsp,const,lp,rev sp_projs)
+    
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 4e0ba6036d..2020a3b26 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -1,12 +1,12 @@
 
 (* $Id$ *)
 
+(*i*)
 open Names
 open Term
+(*i*)
 
 val definition_structure :
-  string * identifier * (identifier * CoqAst.t) list *
-  (bool * (identifier * CoqAst.t)) list * identifier *
-  CoqAst.t -> unit;;
-
-(* $Id$ *)
+  string * identifier * (identifier * Coqast.t) list *
+  (bool * (identifier * Coqast.t)) list * identifier *
+  Coqast.t -> unit
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 20d0a40c1..b19bcabb5 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -15,6 +15,7 @@ open Reduction
 open Pfedit
 open Tacmach
 open Proof_trees
+open Tacred
 open Library
 open Libobject
 open Environ
@@ -704,7 +705,6 @@ let _ =
                        'sTR"failed... aborting" >])
        | _ -> bad_vernac_args "TheoremProof")
 
-(***
 let _ =
   add "DEFINITION"
     (function 
@@ -739,8 +739,8 @@ let _ =
                message ((string_of_id id) ^ " is now a coercion")
 	     end;
 	     if idcoe then 
-	       Class.try_add_new_coercion_subclass stre id;
-             if objdef then Recordobj.objdef_declare id
+	       Class.try_add_new_coercion_subclass id stre;
+             (***TODO if objdef then Recordobj.objdef_declare id ***)
        | _ -> bad_vernac_args "DEFINITION")
 
 let _ =
@@ -772,7 +772,6 @@ let _ =
                     sl)
 	       slcl
        | _ -> bad_vernac_args "VARIABLE")
-  ***)
   
 let _ =
   add "PARAMETER"
@@ -791,15 +790,14 @@ let _ =
                slcl
        | _ -> bad_vernac_args "PARAMETER")
 
-(***
 let _ =
   add "Eval"
     (function
        | VARG_TACTIC_ARG (Redexp (rn,unf)) :: VARG_COMMAND c :: g ->
            let (evmap,sign) = get_evmap_sign (goal_of_args g) in
            let redexp = redexp_of_ast evmap sign (rn,unf) in 
-           let redfun = print_eval (reduction_of_redexp redexp evmap) sign in 
-	   fun () -> mSG (redfun (fconstruct_with_univ evmap sign c))
+           let redfun = print_eval (reduction_of_redexp redexp) sign in 
+	   fun () -> mSG (redfun (judgment_of_com evmap sign c))
        | _ -> bad_vernac_args "Eval")
 
 let _ =
@@ -812,9 +810,10 @@ let _ =
              | "PRINTTYPE" -> print_type
              | _ -> anomaly "Unexpected string" 
 	   in
-	   (fun () -> mSG (prfun sign (fconstruct_with_univ evmap sign c)))
+	   (fun () -> mSG (prfun sign (judgment_of_com evmap sign c)))
        | _ -> bad_vernac_args "Check")
 
+(***
 let _ =
   add "PrintExtractId"
     (function