Réparation bug #888 (les tactiques fix et cofix exigent autant de sous-buts que de fonctions récursives même si l'une de ses fonctions n'a pas de meta); suppression gmm au passage suite commit précédent

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

1 files changed, 26 insertions, 24 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index 88e2fcea8..b7298aa7a 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -89,7 +89,7 @@ and pp_sg sg =
  *  meta_map correspond à celui des buts qui seront engendrés par le refine.
  *)
 
-let replace_by_meta env gmm = function
+let replace_by_meta env = function
   | TH (m, mm, sgp) when isMeta (strip_outer_cast m) -> m,mm,sgp
   | (TH (c,mm,_)) as th ->
       let n = Evarutil.new_meta() in
@@ -101,7 +101,7 @@ let replace_by_meta env gmm = function
 	| Lambda (Anonymous,c1,c2) when isCast c2 ->
 	    mkArrow c1 (snd (destCast c2))
 	| _ -> (* (App _ | Case _) -> *)
-	    Retyping.get_type_of_with_meta env Evd.empty (gmm@mm) c
+	    Retyping.get_type_of_with_meta env Evd.empty mm c
 	(*
 	| Fix ((_,j),(v,_,_)) ->
 	    v.(j) (* en pleine confiance ! *)
@@ -112,23 +112,23 @@ let replace_by_meta env gmm = function
 
 exception NoMeta
 
-let replace_in_array env gmm a =
+let replace_in_array keep_length env a =
   if array_for_all (function (TH (_,_,[])) -> true | _ -> false) a then
     raise NoMeta;
   let a' = Array.map (function
-			| (TH (c,mm,[])) -> c,mm,[]
-			| th -> replace_by_meta env gmm th) a 
+			| (TH (c,mm,[])) when not keep_length -> c,mm,[]
+			| th -> replace_by_meta env th) a 
   in
-  let v' = Array.map (fun (x,_,_) -> x) a' in
-  let mm = Array.fold_left (@) [] (Array.map (fun (_,x,_) -> x) a') in
-  let sgp = Array.fold_left (@) [] (Array.map (fun (_,_,x) -> x) a') in
+  let v' = Array.map pi1 a' in
+  let mm = Array.fold_left (@) [] (Array.map pi2 a') in
+  let sgp = Array.fold_left (@) [] (Array.map pi3 a') in
   v',mm,sgp
     
 let fresh env n =
   let id = match n with Name x -> x | _ -> id_of_string "_" in
   next_global_ident_away true id (ids_of_named_context (named_context env))
 
-let rec compute_metamap env gmm c = match kind_of_term c with
+let rec compute_metamap env c = match kind_of_term c with
   (* le terme est directement une preuve *)
   | (Const _ | Evar _ | Ind _ | Construct _ |
     Sort _ | Var _ | Rel _) -> 
@@ -149,12 +149,12 @@ let rec compute_metamap env gmm c = match kind_of_term c with
   | Lambda (name,c1,c2) ->
       let v = fresh env name in
       let env' = push_named (v,None,c1) env in
-      begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
+      begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
 	(* terme de preuve incomplet *)    
 	| th ->
-	    let m,mm,sgp = replace_by_meta env' gmm th in
+	    let m,mm,sgp = replace_by_meta env' th in
 	    TH (mkLambda (Name v,c1,m), mm, sgp)
       end
 
@@ -163,21 +163,21 @@ let rec compute_metamap env gmm c = match kind_of_term c with
 	error "Refine: body of let-in cannot contain existentials";
       let v = fresh env name in
       let env' = push_named (v,Some c1,t1) env in
-      begin match compute_metamap env' gmm (subst1 (mkVar v) c2) with
+      begin match compute_metamap env' (subst1 (mkVar v) c2) with
 	(* terme de preuve complet *)
 	| TH (_,_,[]) -> TH (c,[],[])
 	(* terme de preuve incomplet *)    
 	| th ->
-	    let m,mm,sgp = replace_by_meta env' gmm th in
+	    let m,mm,sgp = replace_by_meta env' th in
 	    TH (mkLetIn (Name v,c1,t1,m), mm, sgp)
       end
 
   (* 4. Application *)
   | App (f,v) ->
-      let a = Array.map (compute_metamap env gmm) (Array.append [|f|] v) in
+      let a = Array.map (compute_metamap env) (Array.append [|f|] v) in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env gmm a in
+	  let v',mm,sgp = replace_in_array false env a in
           let v'' = Array.sub v' 1 (Array.length v) in
           TH (mkApp(v'.(0), v''),mm,sgp)
 	with NoMeta ->
@@ -188,10 +188,10 @@ let rec compute_metamap env gmm c = match kind_of_term c with
       (* bof... *)
       let nbr = Array.length v in
       let v = Array.append [|p;cc|] v in
-      let a = Array.map (compute_metamap env gmm) v in
+      let a = Array.map (compute_metamap env) v in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env gmm a in
+	  let v',mm,sgp = replace_in_array false env a in
 	  let v'' = Array.sub v' 2 nbr in
 	  TH (mkCase (ci,v'.(0),v'.(1),v''),mm,sgp)
 	with NoMeta ->
@@ -205,12 +205,12 @@ let rec compute_metamap env gmm c = match kind_of_term c with
       let fi' = Array.map (fun id -> Name id) vi in
       let env' = push_named_rec_types (fi',ai,v) env in
       let a = Array.map
-		(compute_metamap env' gmm)
+		(compute_metamap env')
 		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
       in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env' gmm a in
+	  let v',mm,sgp = replace_in_array true env' a in
 	  let fix = mkFix ((ni,i),(fi',ai,v')) in
 	  TH (fix,mm,sgp)
 	with NoMeta ->
@@ -218,7 +218,7 @@ let rec compute_metamap env gmm c = match kind_of_term c with
       end
 	      
   (* Cast. Est-ce bien exact ? *)
-  | Cast (c,t) -> compute_metamap env gmm c
+  | Cast (c,t) -> compute_metamap env c
       (*let TH (c',mm,sgp) = compute_metamap sign c in
 	TH (mkCast (c',t),mm,sgp) *)
       
@@ -235,12 +235,12 @@ let rec compute_metamap env gmm c = match kind_of_term c with
       let fi' = Array.map (fun id -> Name id) vi in
       let env' = push_named_rec_types (fi',ai,v) env in
       let a = Array.map
-		(compute_metamap env' gmm)
+		(compute_metamap env')
 		(Array.map (substl (List.map mkVar (Array.to_list vi))) v) 
       in
       begin
 	try
-	  let v',mm,sgp = replace_in_array env' gmm a in
+	  let v',mm,sgp = replace_in_array true env' a in
 	  let cofix = mkCoFix (i,(fi',ai,v')) in
 	  TH (cofix,mm,sgp)
 	with NoMeta ->
@@ -340,7 +340,9 @@ let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
 let refine oc gl =
   let sigma = project gl in
   let env = pf_env gl in
-  let (gmm,c) = Evarutil.exist_to_meta sigma oc in
-  let th = compute_metamap env gmm c in
+  let (_gmm,c) = Evarutil.exist_to_meta sigma oc in
+  (* Relies on Cast's put on Meta's by exist_to_meta, because it is otherwise 
+     complicated to update gmm when passing through a binder *)
+  let th = compute_metamap env c in
   tcc_aux [] th gl