Correction bug soumis par Yves

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

2 files changed, 13 insertions, 10 deletions

diff --git a/tactics/refine.ml b/tactics/refine.ml
index 5ca8c35889..20621b8e0a 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -253,7 +253,8 @@ let rec compute_metamap env gmm c = match kind_of_term c with
  *  Réalise le 3. ci-dessus
  *)
 
-let rec tcc_aux (TH (c,mm,sgp) as th) gl =
+let rec tcc_aux subst (TH (c,mm,sgp) as th) gl =
+  let c = substl subst c in
   match (kind_of_term c,sgp) with
     (* mv => sous-but : on ne fait rien *)
     | Meta _ , _ ->
@@ -270,7 +271,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
     | Lambda (Name id,_,m), _ when isMeta (strip_outer_cast m) ->
 	begin match sgp with
 	  | [None] -> introduction id gl
-	  | [Some th] -> tclTHEN (introduction id) (tcc_aux th) gl
+	  | [Some th] ->
+              tclTHEN (introduction id)
+                (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th)) gl
 	  | _ -> assert false
 	end
 	
@@ -285,7 +288,9 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	  (change_in_concl None newc) 
 	  (match sgp with 
 	     | [None] -> introduction id
-	     | [Some th] -> tclTHEN (introduction id) (tcc_aux th)
+	     | [Some th] ->
+                 tclTHEN (introduction id)
+                   (onLastHyp (fun id -> tcc_aux (mkVar id::subst) th))
 	     | _ -> assert false) 
 	  gl
 
@@ -304,7 +309,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	    (List.tl (Array.to_list fixes)))
 	  (List.map (function
 		       | None -> tclIDTAC 
-		       | Some th -> tcc_aux th) sgp)
+		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
     (* cofix => tactique CoFix *)
@@ -318,7 +323,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	  (mutual_cofix (out_name fi.(0)) (List.tl (Array.to_list cofixes)))
 	  (List.map (function
 		       | None -> tclIDTAC 
-		       | Some th -> tcc_aux th) sgp)
+		       | Some th -> tcc_aux subst th) sgp)
 	  gl
 
     (* sinon on fait refine du terme puis appels rec. sur les sous-buts.
@@ -326,7 +331,8 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
     | _ ->
 	tclTHENS
 	  (refine c)
-	  (List.map (function None -> tclIDTAC | Some th -> tcc_aux th) sgp)
+	  (List.map
+            (function None -> tclIDTAC | Some th -> tcc_aux subst th) sgp)
 	  gl
 
 (* Et finalement la tactique refine elle-même : *)
@@ -336,5 +342,5 @@ let refine oc gl =
   let env = pf_env gl in
   let (gmm,c) = Clenv.exist_to_meta sigma oc in
   let th = compute_metamap env gmm c in
-  tcc_aux th gl
+  tcc_aux [] th gl
 
diff --git a/tactics/refine.mli b/tactics/refine.mli
index 4f72a26223..c3c73390af 100644
--- a/tactics/refine.mli
+++ b/tactics/refine.mli
@@ -12,6 +12,3 @@ open Term
 open Tacmach
 
 val refine : Pretyping.open_constr -> tactic
-(*
-val refine_tac : Pretyping.open_constr -> tactic
-*)