Changement de la structure des points fixes

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

3 files changed, 15 insertions, 13 deletions

diff --git a/tactics/EAuto.v b/tactics/EAuto.v
index e1ac47ddd8..ba233cdd3a 100644
--- a/tactics/EAuto.v
+++ b/tactics/EAuto.v
@@ -43,7 +43,7 @@ Grammar tactic simple_tactic: ast :=
 | eautod_with_star [ "EAutod" eautoarg($np) "with" "*" ] 
 	-> [(EAuto "debug" ($LIST $np) "*")]
 
-with eautoarg : List :=
+with eautoarg : ast list :=
 | eautoarg_mt [ ] -> [ ]
 | eautoarg_n  [ numarg($n) ] -> [ $n ] 
 | eautoarg_np [ numarg($n) numarg($p) ] -> [ $n $p ] 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index ca64a856ec..2b1c9da35c 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1147,6 +1147,7 @@ let bind_eq = function
   | (Name _,Name _) -> true
   | _ -> false
 
+(* TODO: Fix and CoFix also contain bound names *)
 let eqop_mod_names = function
   | OpLambda n0, OpLambda n1 -> bind_eq (n0,n1)
   | OpProd n0, OpProd n1 -> bind_eq (n0,n1)
diff --git a/tactics/refine.ml b/tactics/refine.ml
index aecc7fbea7..1de41c4894 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -187,21 +187,19 @@ let rec compute_metamap env c = match kind_of_term c with
       end
 
   (* 5. Fix. *)
-  | IsFix ((ni,i),(ai,fi,v)) ->
-      let vi = List.rev (List.map (fresh env) fi) in
-      let env' =
-	List.fold_left (fun env (v,ar) -> push_named_assum (v, ar) env) env
-	  (List.combine vi (Array.to_list ai)) 
-      in
+  | IsFix ((ni,i),(fi,ai,v)) ->
+      (* TODO: use a fold *)
+      let vi = Array.map (fresh env) fi in
+      let fi' = Array.map (fun id -> Name id) vi in
+      let env' = push_rec_types (fi',ai,v) env in
       let a = Array.map
 		(compute_metamap env')
-		(Array.map (substl (List.map mkVar vi)) v) 
+		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
       in
       begin
 	try
 	  let v',mm,sgp = replace_in_array env' a in
-	  let fi' = List.rev (List.map (fun id -> Name id) vi) in
-	  let fix = mkFix ((ni,i),(ai,fi',v')) in
+	  let fix = mkFix ((ni,i),(fi',ai,v')) in
 	  TH (fix,mm,sgp)
 	with NoMeta ->
 	  TH (c,[],[])
@@ -254,10 +252,13 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	error "invalid abstraction passed to function tcc_aux !"
       
     (* fix => tactique Fix *)
-    | IsFix ((ni,_),(ai,fi,_)) , _ ->
+    | IsFix ((ni,_),(fi,ai,_)) , _ ->
 	let ids =
-	  List.map (function Name id -> id | _ ->
-		      error "recursive functions must have names !") fi 
+	  Array.to_list
+            (Array.map
+              (function Name id -> id
+                | _ -> error "recursive functions must have names !")
+              fi) 
 	in
 	tclTHENS
 	  (mutual_fix ids (List.map succ (Array.to_list ni))