Nettoyage de Generic

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

7 files changed, 45 insertions, 47 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 85bce776a6..67d2798674 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -220,12 +220,11 @@ let lift_tomatch_type n = liftn_tomatch_type n 1
 let lift_tomatch n ((current,typ),info) =
   ((lift n current,lift_tomatch_type n typ),info)
 
-let substn_many_tomatch v depth = function
-  | IsInd (t,indt) ->
-      IsInd (substn_many v depth t,substn_many_ind_type v depth indt)
-  | NotInd t -> NotInd (substn_many v depth t)
+let substnl_tomatch v depth = function
+  | IsInd (t,indt) -> IsInd (substnl v depth t,substnl_ind_type v depth indt)
+  | NotInd t -> NotInd (substnl v depth t)
 
-let subst_tomatch (depth,c) = substn_many_tomatch [|make_substituend c|] depth
+let subst_tomatch (depth,c) = substnl_tomatch [c] depth
 
 
 (**********************************************************************)
@@ -361,8 +360,7 @@ let rec lift_subst_tomatch n (depth,ci as binder) = function
   | Pushed (lift,tm)::rest ->
       Pushed (n+lift, tm)::(lift_subst_tomatch n binder rest)
 
-let subst_in_subst id t (id2,c) =
-   (id2,replace_vars [(id,make_substituend t)] c)
+let subst_in_subst id t (id2,c) = (id2,replace_vars [(id,t)] c)
 
 let replace_id_in_rhs id t rhs =
   if List.mem id rhs.private_ids then
@@ -454,9 +452,9 @@ let prepare_unif_pb typ cs =
 
   (* We may need to invert ci if its parameters occur in p *)
   let p' =
-    if noccur_bet 1 n p then lift (-n) p
+    if noccur_between 1 n p then lift (-n) p
     else 
-      (* Il faudrait que noccur_bet ne regarde pas la subst des Evar *)
+      (* Il faudrait que noccur_between ne regarde pas la subst des Evar *)
       if match p with DOPN(Evar _,_) -> true | _ -> false then lift (-n) p
       else failwith "TODO4-1" in
   let ci = applist
@@ -494,15 +492,15 @@ let lift_predicate n pred =
 
 let subst_predicate (args,copt) pred =
   let sigma = match copt with
-    | None -> Array.map make_substituend (Array.of_list args)
-    | Some c -> Array.map make_substituend (Array.of_list (args@[c])) in
+    | None -> args
+    | Some c -> args@[c] in
   let rec substrec k = function
-    | PrCcl ccl -> PrCcl (substn_many sigma k ccl)
+    | PrCcl ccl -> PrCcl (substnl sigma k ccl)
     | PrProd ((dep,na,t),pred) ->
-	PrProd ((dep,na,substn_many_tomatch sigma k t), substrec (k+1) pred)
+	PrProd ((dep,na,substnl_tomatch sigma k t), substrec (k+1) pred)
     | PrLetIn ((args,copt),pred) ->
-	let args' = List.map (substn_many sigma k) args in
-	let copt' = option_app (substn_many sigma k) copt in
+	let args' = List.map (substnl sigma k) args in
+	let copt' = option_app (substnl sigma k) copt in
 	PrLetIn ((args',copt'), substrec (k+1) pred) in
   substrec 0 pred
 
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 901e60b8c8..01ed9dc3bb 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -247,7 +247,7 @@ let computable p k =
 
   let rec striprec = function
     | (0,DOP2(Lambda,_,DLAM(_,d))) -> false
-    | (0,d               )         -> noccur_bet 1 k d
+    | (0,d               )         -> noccur_between 1 k d
     | (n,DOP2(Lambda,_,DLAM(_,d))) -> striprec (n-1,d)
     |  _                           -> false
   in 
@@ -356,8 +356,8 @@ let rec detype avoid env t =
 	    RCases (dummy_loc,tag,pred,[tomatch],eqnl)
 	end
 	
-    | IsFix (nv,n,cl,lfn,vt) -> detype_fix (RFix (nv,n)) avoid env cl lfn vt
-    | IsCoFix (n,cl,lfn,vt)  -> detype_fix (RCofix n) avoid env cl lfn vt)
+    | IsFix (nvn,(cl,lfn,vt)) -> detype_fix (RFix nvn) avoid env cl lfn vt
+    | IsCoFix (n,(cl,lfn,vt))  -> detype_fix (RCofix n) avoid env cl lfn vt)
 
 and detype_fix fk avoid env cl lfn vt =
   let lfi = List.map (fun id -> next_name_away id avoid) lfn in
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 5e89dbc5db..863843d4fa 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -244,7 +244,7 @@ let new_isevar isevars env typ k =
  *)
 let evar_define isevars lhs rhs =
   let (ev,argsv) = destEvar lhs in
-  if occur_opern (Evar ev) rhs then error_occur_check CCI empty_env ev rhs;
+  if occur_evar ev rhs then error_occur_check CCI empty_env ev rhs;
   let args = List.map (function (VAR _ | Rel _) as t -> t | _ -> mkImplicit)
       (Array.to_list argsv) in 
   let evd = ise_map isevars ev in
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 5d64f6e230..2493ae7a09 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -329,15 +329,16 @@ match cstr with   (* Où teste-t-on que le résultat doit satisfaire tycon ? *)
         pretype (mk_tycon (lift nbfix (larj.(i).uj_val))) newenv isevars lvar
           lmeta def) vdef in
   (evar_type_fixpoint env isevars lfi lara vdefj;
-  match fixkind with
-    | RFix(vn,i) ->
-      let fix = mkFix vn i lara (List.rev lfi) (Array.map j_val_only vdefj) in
-	check_fix env !isevars fix;
-	make_judge fix lara.(i)
-    | RCofix i -> 
-      let cofix = mkCoFix i lara (List.rev lfi) (Array.map j_val_only vdefj) in
-	check_cofix env !isevars cofix;
-	make_judge cofix lara.(i))
+   let larav = Array.map body_of_type lara in
+   match fixkind with
+     | RFix (vn,i as vni) ->
+	 let fix = (vni,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+	 check_fix env !isevars fix;
+	 make_judge (mkFix fix) lara.(i)
+     | RCofix i -> 
+	 let cofix = (i,(larav,List.rev lfi,Array.map j_val_only vdefj)) in
+	 check_cofix env !isevars cofix;
+	 make_judge (mkCoFix cofix) lara.(i))
 
 | RSort (loc,s) -> pretype_sort s
 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 96de2fc0ae..e4554527d9 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -64,8 +64,8 @@ let rec type_of env cstr=
     | IsLambda (name,c1,c2) ->
         let var = make_typed c1 (sort_of env c1) in
           mkProd name c1 (type_of (push_rel (name,var) env) c2)
-    | IsFix (vn,i,lar,lfi,vdef) -> lar.(i)
-    | IsCoFix (i,lar,lfi,vdef) -> lar.(i)
+    | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
+    | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
     | IsAppL(f,args)->
       strip_outer_cast (subst_type env sigma (type_of env f) args)
     | IsCast (c,t) -> t
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2f3b674f6a..836b5e3efa 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -85,14 +85,11 @@ let reduce_fix_use_function f whfun fix stack =
 		  | _ -> (false,(fix,stack'))))
     | _ -> assert false
 
-let contract_cofix_use_function f cofix =
-  match cofix with 
-    | DOPN(CoFix(bodynum),bodyvect) ->
-  	let nbodies =  (Array.length bodyvect) -1 in
-  	let make_Fi j = DOPN(CoFix(j),bodyvect) in
-  	let lbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
-  	sAPPViList bodynum (array_last bodyvect) lbodies
-    | _ -> assert false
+let contract_cofix_use_function f (bodynum,(_,_,bodies as typedbodies)) =
+  let nbodies = Array.length bodies in
+  let make_Fi j = mkCoFix (nbodies-j-1,typedbodies) in
+  let subbodies = list_assign (list_tabulate make_Fi nbodies) bodynum f in
+  substl subbodies bodies.(bodynum)
 
 let reduce_mind_case_use_function env f mia =
   match mia.mconstr with 
@@ -101,7 +98,7 @@ let reduce_mind_case_use_function env f mia =
 	let real_cargs = list_lastn ncargs mia.mcargs in
 	applist (mia.mlf.(i-1),real_cargs)
     | DOPN(CoFix _,_) as cofix ->
-	let cofix_def = contract_cofix_use_function f cofix in
+	let cofix_def = contract_cofix_use_function f (destCoFix cofix) in
 	mkMutCaseA mia.mci mia.mP (applist(cofix_def,mia.mcargs)) mia.mlf
     | _ -> assert false
 	  
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 583d395c83..92ad4cf5c6 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -58,19 +58,21 @@ let rec execute mf env sigma cstr =
         let lfj = execute_array mf env sigma lf in
         type_of_case env sigma ci pj cj lfj
   
-    | IsFix (vn,i,lar,lfi,vdef) ->
+    | IsFix ((vn,i as vni),(lar,lfi,vdef)) ->
         if (not mf.fix) && array_exists (fun n -> n < 0) vn then
           error "General Fixpoints not allowed";
-        let larv,vdefv = execute_fix mf env sigma lar lfi vdef in
-        let fix = mkFix vn i larv lfi vdefv in
+        let larjv,vdefv = execute_fix mf env sigma lar lfi vdef in
+ 	let larv = Array.map body_of_type larjv in
+	let fix = vni,(larv,lfi,vdefv) in
         check_fix env sigma fix;
-	make_judge fix larv.(i)
+	make_judge (mkFix fix) larjv.(i)
 	  
-    | IsCoFix (i,lar,lfi,vdef) ->
-        let (larv,vdefv) = execute_fix mf env sigma lar lfi vdef in
-        let cofix = mkCoFix i larv lfi vdefv in
+    | IsCoFix (i,(lar,lfi,vdef)) ->
+        let (larjv,vdefv) = execute_fix mf env sigma lar lfi vdef in
+	let larv = Array.map body_of_type larjv in
+        let cofix = i,(larv,lfi,vdefv) in
         check_cofix env sigma cofix;
-	make_judge cofix larv.(i)
+	make_judge (mkCoFix cofix) larjv.(i)
 	  
     | IsSort (Prop c) -> 
 	judge_of_prop_contents c