From bd1681bdb5830333515de304a72943cb93c09baf Mon Sep 17 00:00:00 2001
From: msozeau
Date: Tue, 18 Oct 2011 09:33:55 +0000
Subject: Fix bug #2586 and enhance clsubst* as well as a side effect

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14570 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/rewrite.ml4                      | 2 +-
 test-suite/bugs/closed/shouldfail/2586.v | 5 +++++
 theories/Classes/SetoidClass.v           | 2 +-
 3 files changed, 7 insertions(+), 2 deletions(-)
 create mode 100644 test-suite/bugs/closed/shouldfail/2586.v

diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index 1595ded2d7..2af439550a 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -1401,7 +1401,7 @@ let clsubstitute o c =
       (fun cl ->
 	match cl with
 	  | Some id when is_tac id -> tclIDTAC
-	  | _ -> tclTRY (cl_rewrite_clause c o all_occurrences cl))
+	  | _ -> cl_rewrite_clause c o all_occurrences cl)
 
 TACTIC EXTEND substitute
 | [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> [ clsubstitute o c ]
diff --git a/test-suite/bugs/closed/shouldfail/2586.v b/test-suite/bugs/closed/shouldfail/2586.v
new file mode 100644
index 0000000000..6111a6415f
--- /dev/null
+++ b/test-suite/bugs/closed/shouldfail/2586.v
@@ -0,0 +1,5 @@
+Require Import Setoid SetoidClass Program.
+
+Goal forall `(Setoid nat) x y, x == y -> S x == S y.
+  intros.
+  clsubst H0.
\ No newline at end of file
diff --git a/theories/Classes/SetoidClass.v b/theories/Classes/SetoidClass.v
index be228f3fea..591671d98f 100644
--- a/theories/Classes/SetoidClass.v
+++ b/theories/Classes/SetoidClass.v
@@ -69,7 +69,7 @@ Notation " x =/= y " := (complement equiv x y) (at level 70, no associativity) :
 (** Use the [clsubstitute] command which substitutes an equality in every hypothesis. *)
 
 Ltac clsubst H :=
-  match type of H with
+  lazymatch type of H with
     ?x == ?y => substitute H ; clear H x
   end.
 
-- 
cgit v1.2.3