Nettoyage

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

2 files changed, 42 insertions, 36 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index f78ab96113..f2c7d0f14c 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -265,17 +265,17 @@ let unify m gls =
 
 let collect_metas c = 
   let rec collrec acc c =
-    match splay_constr c with
-      | OpMeta mv, _ -> mv::acc
-      | _, cl        -> Array.fold_left collrec acc cl
+    match kind_of_term c with
+      | IsMeta mv -> mv::acc
+      | _         -> fold_constr collrec acc c
   in
   List.rev (collrec [] c)
 
 let metavars_of c =  
   let rec collrec acc c =
-    match splay_constr c with
-      | OpMeta mv, _ -> Intset.add mv acc
-      | _, cl       ->  Array.fold_left collrec acc cl
+    match kind_of_term c with
+      | IsMeta mv -> Intset.add mv acc
+      | _         -> fold_constr collrec acc c
   in 
   collrec Intset.empty c
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index cf980cc79b..7fa6c5fee8 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -124,26 +124,32 @@ let build_mutual lparams lnamearconstrs finite =
   and nparams = List.length lparams
   and sigma = Evd.empty 
   and env0 = Global.env() in
-  let mispecvec =
-    let (ind_env,arityl) =
-      List.fold_left 
-	(fun (env,arl) (recname,arityc,_) -> 
-           let raw_arity = mkProdCit lparams arityc in
-           let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
-	   let arity = arj.utj_val in
-	   let env' = Environ.push_rel_assum (Name recname,arity) env in
-	   (env', (arity::arl)))
-	(env0,[]) lnamearconstrs 
-    in
+  let env_params, params =
+    List.fold_left
+      (fun (env, params) (id,t) ->
+	 let p = interp_type sigma env t in
+	 (Environ.push_rel_assum (Name id,p) env, (Name id,p)::params))
+      (env0,[]) lparams
+  in
+  let (ind_env,arityl) =
+    List.fold_left
+      (fun (env,arl) (recname,arityc,_) ->
+         let arity = interp_type sigma env_params arityc in
+	 let fullarity = prod_it arity params in
+	 let env' = Environ.push_rel_assum (Name recname,fullarity) env in
+	 (env', (fullarity::arl)))
+      (env0,[]) lnamearconstrs
+  in
+  let ind_env_params = Environ.push_rels_assum params ind_env in
+  let mispecvec = 
     List.map2
-      (fun ar (name,_,lname_constr) -> 
-         let consconstrl =
-           List.map 
-             (fun (_,constr) -> interp_constr sigma ind_env
-                  (mkProdCit lparams constr))
-             lname_constr 
-	 in
-         (name, (body_of_type ar), List.map fst lname_constr, consconstrl))
+      (fun ar (name,_,lname_constr) ->
+	 let constrnames, bodies = List.split lname_constr in
+         let constrs =
+	   List.map
+	     (fun c -> prod_it (interp_constr sigma ind_env_params c) params)
+	     bodies
+	 in (name, ar, constrnames, constrs))
       (List.rev arityl) lnamearconstrs
   in
   let mie = { 
@@ -204,27 +210,27 @@ let build_recursive lnameargsardef =
       List.fold_left 
         (fun (env,arl) (recname,lparams,arityc,_) -> 
            let raw_arity = mkProdCit lparams arityc in
-           let arj = type_judgment_of_rawconstr Evd.empty env raw_arity in
-	   let arity = arj.utj_val in
+           let arity = interp_type sigma env0 raw_arity in
            declare_variable recname
-	     (SectionLocalAssum arj.utj_val,NeverDischarge,false);
+	     (SectionLocalAssum arity, NeverDischarge, false);
            (Environ.push_named_assum (recname,arity) env, (arity::arl)))
         (env0,[]) lnameargsardef
     with e ->
       States.unfreeze fs; raise e
-  in 
-  let recdef = (* TODO: remplacer mkCast par un appel à interp_casted_constr *)
+  in
+  let arityl = List.rev arityl in
+  let recdef =
     try 
-      List.map (fun (_,lparams,arityc,def) -> 
-                  interp_constr sigma rec_sign 
-                    (mkLambdaCit lparams (mkCastC(def,arityc))))
-        lnameargsardef
-    with e -> 
+      List.map2
+	(fun (_,lparams,_,def) arity ->
+           interp_casted_constr sigma rec_sign (mkLambdaCit lparams def) arity)
+        lnameargsardef arityl
+    with e ->
       States.unfreeze fs; raise e
   in
   States.unfreeze fs;
   let (lnonrec,(lnamerec,ldefrec,larrec,nvrec)) = 
-    collect_non_rec lrecnames recdef (List.rev arityl) (Array.to_list nv) in
+    collect_non_rec lrecnames recdef arityl (Array.to_list nv) in
   let n = NeverDischarge in 
   if lnamerec <> [] then begin
     let recvec =