Changement de comportement du [rewrite ... in H]: Coq échoue si H

apparaît dans le but ou dans l'une des hypothèses (ferme les bugs
#447, #883 et #1228).


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

2 files changed, 61 insertions, 54 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 4ed2613d85..72a1267c37 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -87,29 +87,29 @@ let general_rewrite_bindings_clause cls lft2rgt (c,l) gl =
      break search for a defined setoid relation in head position. *)
   let t = snd (decompose_prod (whd_betaiotazeta ctype)) in 
   let head = if isApp t then fst (destApp t) else t in 
-  if relation_table_mem head && l = NoBindings then 
-    general_s_rewrite_clause cls lft2rgt c [] gl
-  else 
-    (* Original code. In particular, [splay_prod] performs delta-reduction. *)
-    let env = pf_env gl in
-    let sigma = project gl in 
-    let _,t = splay_prod env sigma t in
-    match match_with_equation t with
-      | None -> 
-	  if l = NoBindings
-	  then general_s_rewrite_clause cls lft2rgt c [] gl
-	  else error "The term provided does not end with an equation" 
-      | Some (hdcncl,_) -> 
-          let hdcncls = string_of_inductive hdcncl in 
-	  let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
-          let dir = if cls=None then lft2rgt else not lft2rgt in
-          let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
-          let elim =
-	    try pf_global gl (id_of_string rwr_thm)
-            with Not_found ->
-              error ("Cannot find rewrite principle "^rwr_thm)
-          in 
-	  general_elim_clause cls (c,l) (elim,NoBindings) gl
+    if relation_table_mem head && l = NoBindings then 
+      general_s_rewrite_clause cls lft2rgt c [] gl
+    else 
+      (* Original code. In particular, [splay_prod] performs delta-reduction. *)
+      let env = pf_env gl in
+      let sigma = project gl in 
+      let _,t = splay_prod env sigma t in
+	match match_with_equation t with
+	  | None -> 
+	      if l = NoBindings
+	      then general_s_rewrite_clause cls lft2rgt c [] gl
+	      else error "The term provided does not end with an equation" 
+	  | Some (hdcncl,_) -> 
+              let hdcncls = string_of_inductive hdcncl in 
+	      let suffix = elimination_suffix (elimination_sort_of_clause cls gl) in
+              let dir = if cls=None then lft2rgt else not lft2rgt in
+              let rwr_thm = if dir then hdcncls^suffix^"_r" else hdcncls^suffix in
+              let elim =
+		try pf_global gl (id_of_string rwr_thm)
+		with Not_found ->
+		  error ("Cannot find rewrite principle "^rwr_thm)
+              in 
+		general_elim_clause cls (c,l) (elim,NoBindings) gl
 
 let general_rewrite_bindings = general_rewrite_bindings_clause None
 let general_rewrite l2r c = general_rewrite_bindings l2r (c,NoBindings)
@@ -133,21 +133,21 @@ let general_multi_rewrite l2r c cl =
 	  (tclTRY (general_rewrite_bindings_in l2r id c)) 
 	  (try_do_hyps l)
   in 
-  if cl.concl_occs <> [] then 
-    error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
-  else 
-    tclTHENFIRST 
-      (if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
-      (match cl.onhyps with 
-	 | Some l -> do_hyps l
-	 | None -> 
-	     fun gl -> 
-	       (* try to rewrite in all hypothesis 
-		  (except maybe the rewritten one) *)
-	       let ids = match kind_of_term (fst c) with 
-		 | Var id -> list_remove id (pf_ids_of_hyps gl)
-		 | _ -> pf_ids_of_hyps gl
-	       in try_do_hyps ids gl)
+    if cl.concl_occs <> [] then 
+      error "The \"at\" syntax isn't available yet for the rewrite/replace tactic"
+    else 
+      tclTHENFIRST 
+	(if cl.onconcl then general_rewrite_bindings l2r c else tclIDTAC)
+	(match cl.onhyps with 
+	   | Some l -> do_hyps l
+	   | None -> 
+	       fun gl -> 
+		 (* try to rewrite in all hypothesis 
+		    (except maybe the rewritten one) *)
+		 let ids = match kind_of_term (fst c) with 
+		   | Var id -> list_remove id (pf_ids_of_hyps gl)
+		   | _ -> pf_ids_of_hyps gl
+		 in try_do_hyps ids gl)
 
 
 (* Conditional rewriting, the success of a rewriting is related 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a3c57c6927..433b64c326 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -529,39 +529,46 @@ let apply_without_reduce c gl =
 
 let cut_and_apply c gl =
   let goal_constr = pf_concl gl in 
-  match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
-    | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
-	tclTHENLAST
-	  (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
-	  (apply_term c [mkMeta (new_meta())]) gl
-    | _ -> error "Imp_elim needs a non-dependent product"
+    match kind_of_term (pf_hnf_constr gl (pf_type_of gl c)) with
+      | Prod (_,c1,c2) when not (dependent (mkRel 1) c2) ->
+	  tclTHENLAST
+	    (apply_type (mkProd (Anonymous,c2,goal_constr)) [mkMeta(new_meta())])
+	    (apply_term c [mkMeta (new_meta())]) gl
+      | _ -> error "Imp_elim needs a non-dependent product"
 
 let cut c gl =
   match kind_of_term (hnf_type_of gl c) with
     | Sort _ ->
         let id=next_name_away_with_default "H" Anonymous (pf_ids_of_hyps gl) in
         let t = mkProd (Anonymous, c, pf_concl gl) in
-        tclTHENFIRST
-          (internal_cut_rev id c)
-          (tclTHEN (apply_type t [mkVar id]) (thin [id]))
-          gl
+          tclTHENFIRST
+            (internal_cut_rev id c)
+            (tclTHEN (apply_type t [mkVar id]) (thin [id]))
+            gl
     | _  -> error "Not a proposition or a type"
 
 let cut_intro t = tclTHENFIRST (cut t) intro
 
-let cut_replacing id t tac = 
+(* let cut_replacing id t tac = 
   tclTHENS (cut t)
     [tclORELSE
-      (intro_replacing id) 
-      (tclORELSE (intro_erasing id) (intro_using id));
-     tac (refine_no_check (mkVar id)) ]
+	(intro_replacing id) 
+	(tclORELSE (intro_erasing id) (intro_using id));
+     tac (refine_no_check (mkVar id)) ] *)
+
+(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le
+   but, ou dans une autre hypothèse *)
+let cut_replacing id t tac = 
+  tclTHENS (cut t) [
+      tclORELSE (intro_replacing id) (intro_erasing id); 
+      tac (refine_no_check (mkVar id)) ]
 
 let cut_in_parallel l = 
   let rec prec = function
     | [] -> tclIDTAC 
     | h::t -> tclTHENFIRST (cut h) (prec t)
   in 
-  prec (List.rev l)
+    prec (List.rev l)
 
 (********************************************************************)
 (*               Exact tactics                                      *)
@@ -738,7 +745,7 @@ let general_elim_clause elimtac (c,lbindc) (elimc,lbindelimc) gl =
   let indclause  = make_clenv_binding gl (c,t) lbindc  in
   let elimt      = pf_type_of gl elimc in
   let elimclause = make_clenv_binding gl (elimc,elimt) lbindelimc in 
-  elimtac elimclause indclause gl
+    elimtac elimclause indclause gl
 
 let general_elim c e ?(allow_K=true) =
   general_elim_clause (elimination_clause_scheme allow_K) c e