Nettoyage Recordobj et conséquences

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

1 files changed, 34 insertions, 49 deletions

diff --git a/toplevel/recordobj.ml b/toplevel/recordobj.ml
index dac63126aa..ebdf2bce8a 100755
--- a/toplevel/recordobj.ml
+++ b/toplevel/recordobj.ml
@@ -29,59 +29,44 @@ let typ_lams_of t =
 
 let objdef_err ref =
   errorlabstrm "object_declare"
-    [< Printer.pr_global ref; 'sTR" is not a structure object" >]
-
-let trait t =
-  match kind_of_term t with
-    | IsApp (f,args) ->
-	if (match kind_of_term f with  
-              | IsConst _ | IsMutInd _ | IsVar _ | IsMutConstruct _ -> true    
-	      | _ -> false)
-	then (f,Array.to_list args)
-        else raise Not_found
-    | IsConst _ | IsMutInd _ | IsVar _ | IsMutConstruct _ -> t,[]
-    | _ -> raise Not_found
+    [< pr_id (basename (Global.sp_of_global ref));
+       'sTR" is not a structure object" >]
 
 let objdef_declare ref =
   let sp = match ref with ConstRef sp -> sp | _ -> objdef_err ref in
   let env = Global.env () in
   let v = constr_of_reference ref in
-  let vc =
-    match kind_of_term v with
-      | IsConst cst ->
-	  (match constant_opt_value env cst with
-	     | Some vc -> vc
-	     | None -> objdef_err ref)
-      | _ -> objdef_err ref in
+  let vc = match constant_opt_value env sp with
+    | Some vc -> vc
+    | None -> objdef_err ref in
   let lt,t = decompose_lam vc in
   let lt = List.rev (List.map snd lt) in
-  match kind_of_term t with 
-    | IsApp (f,args) ->
-	let { s_PARAM = p; s_PROJ = lpj } = 
-        (try (find_structure
-		(match kind_of_term f with
-                   | IsMutConstruct (indsp,1) -> indsp
-		   | _ -> objdef_err ref))
-         with _ -> objdef_err ref) in
-        let params, projs =
-	  try list_chop p (Array.to_list args)
-	  with _ -> objdef_err ref in
-        let lps = 
-	  try List.combine lpj projs 
-	  with _ -> objdef_err ref in
-        let comp =
-	  List.fold_left
-	    (fun l (spopt,t) -> (* comp=components *)
-	       match spopt with
-		 | None -> l
-                 | Some sp ->
-		     try (sp, trait t)::l
-                     with Not_found -> l)
-            [] lps in
-        add_anonymous_leaf (inObjDef1 sp);
-        List.iter 
-	  (fun (spi,(ci,l_ui)) -> 
-	     add_new_objdef 
-	       ((ConstRef spi,reference_of_constr ci),v,lt,params,l_ui)) comp
-    | _ -> objdef_err ref
-                 
+  let f,args = match kind_of_term t with
+    | IsApp (f,args) -> f,args 
+    | _ -> objdef_err ref in
+  let { s_PARAM = p; s_PROJ = lpj } = 
+    try (find_structure
+	   (match kind_of_term f with
+              | IsMutConstruct (indsp,1) -> indsp
+	      | _ -> objdef_err ref))
+    with Not_found -> objdef_err ref in
+  let params, projs =
+    try list_chop p (Array.to_list args)
+    with _ -> objdef_err ref in
+  let lps = 
+    try List.combine lpj projs 
+    with _ -> objdef_err ref in
+  let comp =
+    List.fold_left
+      (fun l (spopt,t) -> (* comp=components *)
+	 match spopt with
+	   | None -> l
+           | Some proji_sp ->
+	       let c, args = decomp_app t in
+	       try (ConstRef proji_sp, reference_of_constr c, args) :: l
+               with Not_found -> l)
+      [] lps in
+  add_anonymous_leaf (inObjDef1 sp);
+  List.iter
+    (fun (refi,c,argj) -> add_new_objdef ((refi,c),v,lt,params,argj))
+    comp