Ajout de Record

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

11 files changed, 142 insertions, 164 deletions

diff --git a/.depend b/.depend
index ac0d842998..6dfd64e554 100644
--- a/.depend
+++ b/.depend
@@ -77,6 +77,8 @@ pretyping/cases.debug.cmi: kernel/environ.cmi pretyping/evarutil.cmi \
     kernel/type_errors.cmi 
 pretyping/cases.cmi: kernel/environ.cmi pretyping/evarutil.cmi kernel/evd.cmi \
     kernel/names.cmi pretyping/rawterm.cmi kernel/term.cmi 
+pretyping/class.cmi: pretyping/classops.cmi library/declare.cmi \
+    kernel/names.cmi kernel/term.cmi 
 pretyping/classops.cmi: library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     library/libobject.cmi kernel/names.cmi lib/pp.cmi pretyping/rawterm.cmi \
     kernel/term.cmi 
@@ -156,8 +158,6 @@ tactics/tactics.cmi: proofs/clenv.cmi parsing/coqast.cmi kernel/environ.cmi \
 tactics/termdn.cmi: tactics/dn.cmi kernel/generic.cmi kernel/term.cmi 
 tactics/wcclausenv.cmi: proofs/clenv.cmi kernel/evd.cmi kernel/names.cmi \
     proofs/proof_trees.cmi kernel/sign.cmi proofs/tacmach.cmi kernel/term.cmi 
-toplevel/class.cmi: pretyping/classops.cmi library/declare.cmi \
-    kernel/names.cmi kernel/term.cmi 
 toplevel/command.cmi: parsing/coqast.cmi library/declare.cmi kernel/names.cmi \
     pretyping/tacred.cmi kernel/term.cmi 
 toplevel/errors.cmi: parsing/coqast.cmi lib/pp.cmi 
@@ -499,6 +499,16 @@ pretyping/cases.cmx: kernel/environ.cmx pretyping/evarconv.cmx \
     pretyping/retyping.cmx kernel/sign.cmx kernel/term.cmx \
     kernel/type_errors.cmx kernel/typeops.cmx lib/util.cmx \
     pretyping/cases.cmi 
+pretyping/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
+    library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
+    library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
+    library/lib.cmi kernel/names.cmi lib/pp.cmi pretyping/retyping.cmi \
+    kernel/term.cmi pretyping/typing.cmi lib/util.cmi pretyping/class.cmi 
+pretyping/class.cmx: pretyping/classops.cmx kernel/constant.cmx \
+    library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
+    library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \
+    library/lib.cmx kernel/names.cmx lib/pp.cmx pretyping/retyping.cmx \
+    kernel/term.cmx pretyping/typing.cmx lib/util.cmx pretyping/class.cmi 
 pretyping/classops.cmo: library/declare.cmi kernel/environ.cmi \
     kernel/generic.cmi library/lib.cmi library/libobject.cmi kernel/names.cmi \
     lib/options.cmi lib/pp.cmi pretyping/rawterm.cmi library/summary.cmi \
@@ -825,16 +835,6 @@ tactics/wcclausenv.cmx: proofs/clenv.cmx kernel/environ.cmx kernel/evd.cmx \
     proofs/tacmach.cmx kernel/term.cmx lib/util.cmx tactics/wcclausenv.cmi 
 tools/coqdep.cmo: config/coq_config.cmi 
 tools/coqdep.cmx: config/coq_config.cmx 
-toplevel/class.cmo: pretyping/classops.cmi kernel/constant.cmi \
-    library/declare.cmi kernel/environ.cmi kernel/evd.cmi kernel/generic.cmi \
-    library/global.cmi kernel/inductive.cmi kernel/instantiate.cmi \
-    library/lib.cmi kernel/names.cmi lib/pp.cmi pretyping/retyping.cmi \
-    kernel/term.cmi pretyping/typing.cmi lib/util.cmi toplevel/class.cmi 
-toplevel/class.cmx: pretyping/classops.cmx kernel/constant.cmx \
-    library/declare.cmx kernel/environ.cmx kernel/evd.cmx kernel/generic.cmx \
-    library/global.cmx kernel/inductive.cmx kernel/instantiate.cmx \
-    library/lib.cmx kernel/names.cmx lib/pp.cmx pretyping/retyping.cmx \
-    kernel/term.cmx pretyping/typing.cmx lib/util.cmx toplevel/class.cmi 
 toplevel/command.cmo: parsing/ast.cmi parsing/astterm.cmi kernel/constant.cmi \
     parsing/coqast.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi library/indrec.cmi \
@@ -865,14 +865,14 @@ toplevel/coqtop.cmx: config/coq_config.cmx toplevel/coqinit.cmx \
     toplevel/mltop.cmi lib/options.cmx lib/pp.cmx lib/profile.cmx \
     library/states.cmx lib/system.cmx toplevel/toplevel.cmx \
     toplevel/usage.cmx lib/util.cmx toplevel/vernac.cmx toplevel/coqtop.cmi 
-toplevel/discharge.cmo: toplevel/class.cmi pretyping/classops.cmi \
+toplevel/discharge.cmo: pretyping/class.cmi pretyping/classops.cmi \
     kernel/constant.cmi library/declare.cmi kernel/environ.cmi kernel/evd.cmi \
     kernel/generic.cmi library/global.cmi kernel/inductive.cmi \
     kernel/instantiate.cmi library/lib.cmi library/libobject.cmi \
     kernel/names.cmi lib/options.cmi lib/pp.cmi pretyping/recordops.cmi \
     kernel/reduction.cmi kernel/sign.cmi library/summary.cmi kernel/term.cmi \
     kernel/typeops.cmi lib/util.cmi toplevel/discharge.cmi 
-toplevel/discharge.cmx: toplevel/class.cmx pretyping/classops.cmx \
+toplevel/discharge.cmx: pretyping/class.cmx pretyping/classops.cmx \
     kernel/constant.cmx library/declare.cmx kernel/environ.cmx kernel/evd.cmx \
     kernel/generic.cmx library/global.cmx kernel/inductive.cmx \
     kernel/instantiate.cmx library/lib.cmx library/libobject.cmx \
@@ -925,11 +925,15 @@ toplevel/protectedtoplevel.cmo: toplevel/errors.cmi parsing/pcoq.cmi \
 toplevel/protectedtoplevel.cmx: toplevel/errors.cmx parsing/pcoq.cmx \
     lib/pp.cmx toplevel/vernac.cmx toplevel/vernacinterp.cmx \
     toplevel/protectedtoplevel.cmi 
-toplevel/record.cmo: parsing/ast.cmi toplevel/class.cmi parsing/coqast.cmi \
-    library/declare.cmi library/global.cmi kernel/names.cmi lib/pp.cmi \
+toplevel/record.cmo: parsing/ast.cmi parsing/astterm.cmi pretyping/class.cmi \
+    toplevel/command.cmi kernel/constant.cmi parsing/coqast.cmi \
+    library/declare.cmi kernel/environ.cmi kernel/generic.cmi \
+    library/global.cmi kernel/names.cmi lib/pp.cmi pretyping/recordops.cmi \
     kernel/term.cmi lib/util.cmi toplevel/record.cmi 
-toplevel/record.cmx: parsing/ast.cmx toplevel/class.cmx parsing/coqast.cmx \
-    library/declare.cmx library/global.cmx kernel/names.cmx lib/pp.cmx \
+toplevel/record.cmx: parsing/ast.cmx parsing/astterm.cmx pretyping/class.cmx \
+    toplevel/command.cmx kernel/constant.cmx parsing/coqast.cmx \
+    library/declare.cmx kernel/environ.cmx kernel/generic.cmx \
+    library/global.cmx kernel/names.cmx lib/pp.cmx pretyping/recordops.cmx \
     kernel/term.cmx lib/util.cmx toplevel/record.cmi 
 toplevel/toplevel.cmo: parsing/ast.cmi toplevel/errors.cmi toplevel/mltop.cmi \
     lib/options.cmi parsing/pcoq.cmi proofs/pfedit.cmi lib/pp.cmi \
@@ -950,31 +954,33 @@ toplevel/vernac.cmx: parsing/ast.cmx parsing/coqast.cmx library/library.cmx \
     library/states.cmx lib/system.cmx lib/util.cmx toplevel/vernacinterp.cmx \
     toplevel/vernac.cmi 
 toplevel/vernacentries.cmo: parsing/ast.cmi parsing/astterm.cmi \
-    toplevel/class.cmi toplevel/command.cmi parsing/coqast.cmi \
+    pretyping/class.cmi toplevel/command.cmi parsing/coqast.cmi \
     library/declare.cmi toplevel/discharge.cmi kernel/environ.cmi \
     kernel/evd.cmi parsing/extend.cmi library/global.cmi library/goptions.cmi \
     library/impargs.cmi library/lib.cmi library/libobject.cmi \
     library/library.cmi proofs/macros.cmi toplevel/metasyntax.cmi \
     kernel/names.cmi library/nametab.cmi lib/options.cmi parsing/pcoq.cmi \
     proofs/pfedit.cmi lib/pp.cmi lib/pp_control.cmi parsing/pretty.cmi \
-    parsing/printer.cmi proofs/proof_trees.cmi kernel/reduction.cmi \
-    proofs/refiner.cmi lib/stamps.cmi library/states.cmi lib/system.cmi \
-    proofs/tacinterp.cmi proofs/tacmach.cmi pretyping/tacred.cmi \
-    tactics/tactics.cmi kernel/term.cmi kernel/typeops.cmi lib/util.cmi \
-    toplevel/vernacinterp.cmi toplevel/vernacentries.cmi 
+    parsing/printer.cmi proofs/proof_trees.cmi toplevel/record.cmi \
+    kernel/reduction.cmi proofs/refiner.cmi lib/stamps.cmi library/states.cmi \
+    lib/system.cmi proofs/tacinterp.cmi proofs/tacmach.cmi \
+    pretyping/tacred.cmi tactics/tactics.cmi kernel/term.cmi \
+    kernel/typeops.cmi lib/util.cmi toplevel/vernacinterp.cmi \
+    toplevel/vernacentries.cmi 
 toplevel/vernacentries.cmx: parsing/ast.cmx parsing/astterm.cmx \
-    toplevel/class.cmx toplevel/command.cmx parsing/coqast.cmx \
+    pretyping/class.cmx toplevel/command.cmx parsing/coqast.cmx \
     library/declare.cmx toplevel/discharge.cmx kernel/environ.cmx \
     kernel/evd.cmx parsing/extend.cmx library/global.cmx library/goptions.cmx \
     library/impargs.cmx library/lib.cmx library/libobject.cmx \
     library/library.cmx proofs/macros.cmx toplevel/metasyntax.cmx \
     kernel/names.cmx library/nametab.cmx lib/options.cmx parsing/pcoq.cmx \
     proofs/pfedit.cmx lib/pp.cmx lib/pp_control.cmx parsing/pretty.cmx \
-    parsing/printer.cmx proofs/proof_trees.cmx kernel/reduction.cmx \
-    proofs/refiner.cmx lib/stamps.cmx library/states.cmx lib/system.cmx \
-    proofs/tacinterp.cmx proofs/tacmach.cmx pretyping/tacred.cmx \
-    tactics/tactics.cmx kernel/term.cmx kernel/typeops.cmx lib/util.cmx \
-    toplevel/vernacinterp.cmx toplevel/vernacentries.cmi 
+    parsing/printer.cmx proofs/proof_trees.cmx toplevel/record.cmx \
+    kernel/reduction.cmx proofs/refiner.cmx lib/stamps.cmx library/states.cmx \
+    lib/system.cmx proofs/tacinterp.cmx proofs/tacmach.cmx \
+    pretyping/tacred.cmx tactics/tactics.cmx kernel/term.cmx \
+    kernel/typeops.cmx lib/util.cmx toplevel/vernacinterp.cmx \
+    toplevel/vernacentries.cmi 
 toplevel/vernacinterp.cmo: parsing/ast.cmi parsing/coqast.cmi lib/dyn.cmi \
     toplevel/himsg.cmi kernel/names.cmi lib/options.cmi lib/pp.cmi \
     proofs/proof_trees.cmi proofs/tacinterp.cmi lib/util.cmi \
diff --git a/Makefile b/Makefile
index 2d651d905c..af53a8121d 100644
--- a/Makefile
+++ b/Makefile
@@ -76,7 +76,7 @@ LIBRARY=library/libobject.cmo library/summary.cmo library/lib.cmo \
 PRETYPING=pretyping/rawterm.cmo pretyping/detyping.cmo \
 	  pretyping/tacred.cmo pretyping/pretype_errors.cmo \
           pretyping/retyping.cmo pretyping/typing.cmo \
-	  pretyping/classops.cmo pretyping/recordops.cmo \
+	  pretyping/classops.cmo pretyping/class.cmo pretyping/recordops.cmo \
 	  pretyping/evarutil.cmo pretyping/evarconv.cmo \
           pretyping/coercion.cmo pretyping/cases.cmo pretyping/pretyping.cmo \
 	  pretyping/syntax_def.cmo
@@ -101,7 +101,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 toplevel/class.cmo \
+         toplevel/metasyntax.cmo toplevel/command.cmo toplevel/record.cmo \
          toplevel/discharge.cmo \
          toplevel/vernacentries.cmo toplevel/vernac.cmo toplevel/mltop.cmo \
 	 toplevel/protectedtoplevel.cmo toplevel/toplevel.cmo \
diff --git a/toplevel/class.ml b/pretyping/class.ml
index 2262d00835..9b5a02c6f5 100644
--- a/toplevel/class.ml
+++ b/pretyping/class.ml
@@ -174,24 +174,7 @@ l'indice de la classe source dans la liste lp
 la liste des variables dont depend la classe source
 *)
 
-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
-      | 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 ->
 	let (v1,lv1,l,cl1,p1) as x =
@@ -202,14 +185,16 @@ let get_source lp source =
                 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_IND (sp1,i) -> sp=sp1
-               | _ -> false)
+    | Some id -> 
+	let rec aux n = function
+	  | [] -> raise Not_found
+	  | t1::lt ->
+	      try 
+		let v1,lv1,l,cl1,p1 = constructor_at_head1 t1 in
+		if id_of_cl cl1 = id then cl1,p1,v1,lv1,n,l
+		else aux (n+1) lt
+              with _ -> aux (n + 1) lt
+	in id, aux 1 lp
 
 let get_target t ind =
   if (ind > 1) then 
@@ -377,17 +362,17 @@ let try_add_new_coercion id stre =
 
 let try_add_new_coercion_subclass id stre =
   let idf = build_id_coercion None id in
-  try_add_new_coercion_core idf stre (Some (Ident id)) None true
+  try_add_new_coercion_core idf stre (Some id) None true
 
 let try_add_new_coercion_with_target id stre source target isid =
   if isid then
     let idf = build_id_coercion (Some id) source in
-    try_add_new_coercion_core idf stre (Some (Ident source)) (Some target) true
+    try_add_new_coercion_core idf stre (Some source) (Some target) true
   else 
-    try_add_new_coercion_core id stre (Some (Ident source)) (Some target) false
+    try_add_new_coercion_core id stre (Some source) (Some target) false
 
-let try_add_new_coercion_record id stre source_sp =
-  try_add_new_coercion_core id stre (Some (Section_path source_sp)) None false
+let try_add_new_coercion_record id stre source =
+  try_add_new_coercion_core id stre (Some source) None false
 
 (* fonctions pour le discharge: plutot sale *)
 
diff --git a/toplevel/class.mli b/pretyping/class.mli
index f828215548..dc19ccce01 100644
--- a/toplevel/class.mli
+++ b/pretyping/class.mli
@@ -12,7 +12,7 @@ open Declare
 
 val try_add_new_coercion : identifier -> strength -> unit
 val try_add_new_coercion_subclass : identifier -> strength -> unit
-val try_add_new_coercion_record: identifier -> strength -> section_path -> unit
+val try_add_new_coercion_record : identifier -> strength -> identifier -> unit
 val try_add_new_coercion_with_target : identifier -> strength ->
   identifier -> identifier -> bool -> unit
 
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index dea95d0e04..911df0a8aa 100755
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -32,7 +32,7 @@ type struc_typ = {
   s_PARAM : int;
   s_PROJ : section_path option list }
 
-let sTRUCS = (ref [] : (section_path * struc_typ) list ref)
+let sTRUCS = (ref [] : (inductive_path * struc_typ) list ref)
 
 let add_new_struc1 x = sTRUCS:=x::(!sTRUCS)
 
@@ -46,8 +46,6 @@ let (inStruc,outStruc) =
 let add_new_struc (s,c,n,l) = 
   Lib.add_anonymous_leaf (inStruc (s,{s_CONST=c;s_PARAM=n;s_PROJ=l}))
 
-let struc_info s = List.assoc s !sTRUCS
-
 
 (*** table des definitions "object" : pour chaque object c,
 c := [x1:B1]...[xk:Bk](R_Cons a1...am t1...t_n)
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 9b666513f7..5872bd9225 100755
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -23,8 +23,7 @@ type struc_typ = {
   s_PROJ : section_path option list }
 
 val add_new_struc : 
-  section_path * identifier * int * section_path option list -> unit
-val struc_info : section_path -> struc_typ
+  inductive_path * identifier * int * section_path option list -> unit
 
 type obj_typ = {
   o_DEF : constr;
@@ -32,17 +31,14 @@ 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 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 inStruc : inductive_path * struc_typ -> obj
+val outStruc : obj -> inductive_path * struc_typ
 val inObjDef1 : section_path -> obj
 val outObjDef1 : obj -> section_path
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 04fdd2e399..e62e85d57d 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -134,15 +134,16 @@ let build_mutual lparams lnamearconstrs finite =
   and nparams = List.length lparams
   and sigma = Evd.empty 
   and env0 = Global.env() in
-  let fs = States.freeze() in
+(*  let fs = States.freeze() in*)
   try
     let mispecvec =
-      let (ind_sign,arityl) =
+      let (ind_env,arityl) =
       	List.fold_left 
 	  (fun (env,arl) (recname,arityc,_) -> 
              let arity = type_of_com env (mkProdCit lparams arityc) in
 	     let env' = Environ.push_var (recname,arity) env in
-	     declare_variable recname (arity.body,NeverDischarge,false);
+(*	A quoi cela sert ?
+	declare_variable recname (arity.body,NeverDischarge,false);*)
 	     (env', (arity::arl)))
 	  (env0,[]) lnamearconstrs 
       in
@@ -150,27 +151,27 @@ let build_mutual lparams lnamearconstrs finite =
         (fun ar (name,_,lname_constr) -> 
            let consconstrl =
              List.map 
-               (fun (_,constr) -> constr_of_com sigma ind_sign
+               (fun (_,constr) -> constr_of_com sigma ind_env
                     (mkProdCit lparams constr))
                lname_constr 
 	   in
            (name, ar.body, List.map fst lname_constr,
             put_DLAMSV_subst (List.rev lrecnames) (Array.of_list consconstrl)))
         (List.rev arityl) lnamearconstrs
-    in 
+    in
     let mie = { 
       mind_entry_nparams = nparams;
       mind_entry_finite = finite;
       mind_entry_inds = mispecvec }
     in
-    States.unfreeze fs;
+(*    States.unfreeze fs;*)
     let sp = declare_mind mie in
     if is_verbose() then pPNL(minductive_message lrecnames);
     for i = 0 to List.length mispecvec - 1 do
       declare_eliminations sp i
     done
   with e ->
-    States.unfreeze fs; raise e
+(*    States.unfreeze fs; *)raise e
 
 
 (* try to find non recursive definitions *)
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 2942e7e5a3..f57ddb3787 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -201,7 +201,7 @@ type discharge_operation =
   | Constant of identifier * constant_entry * strength
   | Inductive of mutual_inductive_entry
   | Class of cl_typ * cl_info_typ
-  | Struc of section_path * struc_typ
+  | Struc of inductive_path * struc_typ
   | Coercion of ((coe_typ * coe_info_typ) * cl_typ * cl_typ) 
               * identifier * int 
 
@@ -261,14 +261,14 @@ let process_object oldenv sec_sp (ops,ids_to_discard,work_alist) (sp,lobj) =
           ((Coercion (y,idf,ps))::ops, ids_to_discard, work_alist)
                     
     | "STRUCTURE" ->
-	let (sp,info) = outStruc lobj in
+	let ((sp,i),info) = outStruc lobj in
 	let newsp = recalc_sp sp in
 	let mib = Environ.lookup_mind newsp oldenv in
 	let strobj =
 	  { s_CONST = info.s_CONST;
 	    s_PARAM = mib.mind_nparams;
 	    s_PROJ = List.map (option_app recalc_sp) info.s_PROJ } in
-	((Struc (newsp,strobj))::ops, ids_to_discard, work_alist)
+	((Struc ((newsp,i),strobj))::ops, ids_to_discard, work_alist)
 
     (***TODO
     | "OBJDEF1" -> 
diff --git a/toplevel/record.ml b/toplevel/record.ml
index 99cbac0b8b..1a5536a230 100644
--- a/toplevel/record.ml
+++ b/toplevel/record.ml
@@ -4,16 +4,13 @@
 open Pp
 open Util
 open Names
+open Generic
 open Term
+open Declare
 open Coqast
 open Ast
-(*
-open Generic
+open Astterm
 open Command
-open Machops
-open Classops
-open Recordops
-*)
 
 (********** definition d'un record (structure) **************)
 
@@ -69,94 +66,92 @@ 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
-  let sign1,newps =
+  let env0 = Global.env () in
+  let env1,newps =
     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 
+      (fun (env,newps) (id,t) -> 
+         let tj = type_of_com env t in
+         (Environ.push_var (id,tj) env,(id,tj.body)::newps))
+      (env0,[]) ps
   in
-  let sign2,newfs =
+  let env2,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
+      (fun (env,newfs) (id,t) -> 
+         let tj = type_of_com env t in
+         (Environ.push_var (id,tj) env,(id,tj.body)::newfs)) (env1,[]) 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
-  if not (free_in_asts struc tyfs) then 
+let warning_or_error coe st = 
+  if coe then errorlabstrm "structure" st;
+  pPNL [< 'sTR"Warning: "; st >] 
+
+(* Fields have names [idfs] and types [tyfs]; [coers] is a boolean list 
+   telling if the corresponding field must me a coercion *)
+
+let definition_structure (is_coe,idstruc,ps,cfs,idbuild,s) =
+  let coers,fs = List.split cfs in     
+  let idps,typs = List.split ps in      
+  let idfs,tyfs = List.split fs in
+  if not (free_in_asts idstruc 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
+    ope("APPLISTEXPL",
+        (nvar (string_of_id idstruc))::
+        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 _ = build_mutual ps [(idstruc,s,[(idbuild,type_constructor)])] true in
+  let r = global_reference CCI idstruc in
+  let rsp = op_of_mind r in
+  let x = Environ.named_hd (Global.env()) r Anonymous in
+  let lp = List.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) -> 
+
+  (* We build projections *)
+  let (sp_projs,_,_) =
+    List.fold_left2
+      (fun (sp_projs,ids_not_ok,subst) coe (fi,ti) -> 
 	 let fv_ti = global_vars ti in
-	 let bad_projs = (intersect ids_not_ok fv_ti) in
+	 let bad_projs = (list_intersect ids_not_ok fv_ti) in
 	 if bad_projs <> [] then begin 
-	   (warning_or_error (hd coes)
+	   (warning_or_error coe
               [< '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))
+           (None::sp_projs,fi::ids_not_ok,subst)
          end else 
-	   let p = mkNamedLambda x rp2 (replace_vars sigma ti) in
+	   let p = mkLambda x rp2 (replace_vars subst ti) in
 	   let branch = mk_LambdaCit newfs (VAR fi) in
 	   let proj = mk_LambdaCit newps 
-			(mkNamedLambda x rp1 
+			(mkLambda 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)
+	     try
+	       let cie =
+		 { Constant.const_entry_body = Constant.Cooked proj;
+		   Constant.const_entry_type = None } in
+	       (declare_constant fi (cie,NeverDischarge); true)
              with UserError(s,pps) ->
-               ((warning_or_error (hd coes) 
+               ((warning_or_error coe 
                    [<'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))
+	     (None::sp_projs,fi::ids_not_ok,subst)
 	   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))
+             if coe then
+	       Class.try_add_new_coercion_record fi NeverDischarge idstruc;
+             let constr_fi = global_reference CCI fi in
+             let constr_fip = (* Rel 1 refers to "x" *)
+               applist (constr_fi,(List.map (fun id -> VAR id) idps)@[Rel 1])
+             in (Some(path_of_const constr_fi)::sp_projs,
+		 ids_not_ok,
+		 (fi,{sinfo=Closed;sit=constr_fip})::subst)
 	   end)
-      ([],[],[],[],coers) newfs
+      ([],[],[]) coers newfs
   in 
-  if coe_constr="COERCION" then 
-    Class.try_add_new_coercion const NeverDischarge;
-  add_new_struc (rsp,const,lp,rev sp_projs)
-    
+  if is_coe then Class.try_add_new_coercion idbuild NeverDischarge;
+  Recordops.add_new_struc (rsp,idbuild,lp,List.rev sp_projs)
diff --git a/toplevel/record.mli b/toplevel/record.mli
index 2020a3b26b..842754b9ad 100644
--- a/toplevel/record.mli
+++ b/toplevel/record.mli
@@ -7,6 +7,6 @@ open Term
 (*i*)
 
 val definition_structure :
-  string * identifier * (identifier * Coqast.t) list *
+   bool * 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 4dad9e2bc1..54629fe2d3 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -962,7 +962,6 @@ let _ =
 	   fun () -> build_mutual la lnamearconstructs (isfinite f)
        | _ -> bad_vernac_args "MUTUALINDUCTIVE")
 
-(***
 let _ =
   add "RECORD"
     (function
@@ -973,23 +972,21 @@ let _ =
           VARG_VARGLIST namec; 
           VARG_VARGLIST cfs] -> 
            let ps = join_binders binders in
-           let cfs = List.map
-                       (function 
-			  | (VARG_VARGLIST 
-                               [VARG_STRING str;VARG_IDENTIFIER id;
-                                VARG_CONSTR c]) ->
-			      (str = "COERCION",(id,c))
-			  | _ -> bad_vernac_args "RECORD")
-                       cfs 
-	   in
+           let cfs =
+	     List.map
+               (function 
+		  | (VARG_VARGLIST 
+                       [VARG_STRING str; VARG_IDENTIFIER id; VARG_CONSTR c]) ->
+		      (str = "COERCION",(id,c))
+		  | _ -> bad_vernac_args "RECORD")
+               cfs in
            let const = match namec with 
              | [] -> (id_of_string ("Build_"^(string_of_id struc)))
              | [VARG_IDENTIFIER id] -> id 
-             | _ -> bad_vernac_args "RECORD"
-           in 
-	   fun () -> definition_structure (coe,struc,ps,cfs,const,s)
+             | _ -> bad_vernac_args "RECORD" in
+           let iscoe = (coe = "COERCION") in
+	   fun () -> Record.definition_structure (iscoe,struc,ps,cfs,const,s)
        | _ -> bad_vernac_args "RECORD")
-***)
 
 let _ =
   add "MUTUALRECURSIVE"