Modification mkAppL; abstraction via kind_of_term; changement dans Reduction

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

3 files changed, 15 insertions, 19 deletions

diff --git a/library/declare.ml b/library/declare.ml
index 5d62f067a..33fb0f284 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -314,15 +314,11 @@ let global_reference kind id =
 
 let global_reference_imps kind id =
   let c = global_reference kind id in
-  match c with
-    | DOPN (Const sp,_) -> 
-	c, list_of_implicits (constant_implicits sp)
-    | DOPN (MutInd (sp,i),_) -> 
-	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 id
+  match kind_of_term c with
+    | IsConst (sp,_) -> c, list_of_implicits (constant_implicits sp)
+    | IsMutInd (isp,_) -> c, list_of_implicits (inductive_implicits isp)
+    | IsMutConstruct (csp,_) ->	c,list_of_implicits (constructor_implicits csp)
+    | IsVar id -> c, implicits_of_var id
     | _ -> assert false
 (*
 let global env id =
diff --git a/library/indrec.ml b/library/indrec.ml
index 655db9af7..59e11cbff 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -93,14 +93,14 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
   let st = hnf_prod_appvect env sigma t vargs in
   let process_pos depK pk = 
     let rec prec i p = 
-      let p',largs = whd_betadeltaiota_stack env sigma p [] in
+      let p',largs = whd_betadeltaiota_stack env sigma p in
       match kind_of_term p' with
 	| IsProd (n,t,c) -> assert (largs=[]); make_prod env (n,t,prec (i+1) c)
      	| IsMutInd (_,_) -> 
 	    let (_,realargs) = list_chop nparams largs in 
 	    let base = applist (lift i pk,realargs) in       
             if depK then 
-	      mkAppList base [appvect (Rel (i+1),rel_vect 0 i)]
+	      mkAppL (base, [|appvect (Rel (i+1),rel_vect 0 i)|])
             else 
 	      base
       	| _ -> assert false 
@@ -108,7 +108,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
     prec 0 
   in
   let rec process_constr i c recargs co = 
-    let c', largs = whd_betadeltaiota_stack env sigma c [] in
+    let c', largs = whd_betadeltaiota_stack env sigma c in
     match kind_of_term c' with 
       | IsProd (n,t,c_0) ->
 	  assert (largs = []);
@@ -124,20 +124,20 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
           (match optionpos with 
 	     | None -> 
 		 make_prod env (n,t,process_constr (i+1) c_0 rest 
-				  (mkAppList (lift 1 co) [Rel 1]))
+				  (mkAppL (lift 1 co, [|Rel 1|])))
              | Some(dep',p) -> 
 		 let nP = lift (i+1+decP) p in
 		 let t_0 = process_pos dep' nP (lift 1 t) in 
 		 make_prod_dep (dep or dep') env
                    (n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
-				       (mkAppList (lift 2 co) [Rel 2]))))
+				       (mkAppL (lift 2 co, [|Rel 2|])))))
       | IsMutInd ((_,tyi),_) -> 
       	  let nP = match depPvect.(tyi) with 
 	    | Some(_,p) -> lift (i+decP) p
 	    | _ -> assert false in
       	  let (_,realargs) = list_chop nparams largs in
       	  let base = applist (nP,realargs) in
-          if dep then mkAppList base [co] else base
+          if dep then mkAppL (base, [|co|]) else base
       | _ -> assert false
   in 
   process_constr 0 st recargs (appvect(co,vargs))
@@ -145,7 +145,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
 let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs = 
   let process_pos fk  =
     let rec prec i p =
-      let p',largs = whd_betadeltaiota_stack env sigma p [] in
+      let p',largs = whd_betadeltaiota_stack env sigma p in
       match kind_of_term p' with
 	| IsProd (n,t,c) -> lambda_name env (n,t,prec (i+1) c)
      	| IsMutInd _ -> 
@@ -170,14 +170,14 @@ let make_rec_branch_arg env sigma (nparams,fvect,decF) f cstr recargs =
            | None -> 
 	       lambda_name env
 		 (n,incast_type t,process_constr (i+1)
-		    (applist(whd_beta_stack (lift 1 f) [(Rel 1)]))
+		    (whd_beta (applist (lift 1 f, [(Rel 1)])))
 		    (cprest,rest))
            | Some(_,f_0) -> 
 	       let nF = lift (i+1+decF) f_0 in
 	       let arg = process_pos nF (lift 1 (body_of_type t)) in 
                lambda_name env
 		 (n,incast_type t,process_constr (i+1)
-		    (applist(whd_beta_stack (lift 1 f) [(Rel 1); arg])) 
+		    (whd_beta (applist (lift 1 f, [(Rel 1); arg])))
 		    (cprest,rest)))
     | (n,Some c,t)::cprest, rest -> failwith "TODO"
     | [],[] -> f
diff --git a/library/redinfo.ml b/library/redinfo.ml
index 6bd08a2ff..ecd977e56 100644
--- a/library/redinfo.ml
+++ b/library/redinfo.ml
@@ -30,7 +30,7 @@ exception Elimconst
 
 let compute_consteval c = 
   let rec srec n labs c =
-    let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c [] in
+    let c',l = whd_betadeltaeta_stack (Global.env()) Evd.empty c in
     match kind_of_term c' with
       | IsLambda (_,t,g) when l=[] -> srec (n+1) (t::labs) g
       | IsFix ((nv,i),(tys,_,bds)) ->