From e961ace331ec961dcec0e2525d7b9142d04b5154 Mon Sep 17 00:00:00 2001 From: msozeau Date: Sun, 27 Apr 2008 11:16:15 +0000 Subject: - Fix bug in unification not taking into account the right meta substitution. Makes unification succeed a bit more often, hence auto works better in some cases. - Backtrack the changes of auto using Hint Unfold to do more delta and add a new tactic "new auto" which does that, for compatibility. The first fix may have a big impact on the contribs, whereas the second should make them compile again... we'll see. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10855 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Strings/String.v | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'theories/Strings') diff --git a/theories/Strings/String.v b/theories/Strings/String.v index 4057ba022..6826e0c51 100644 --- a/theories/Strings/String.v +++ b/theories/Strings/String.v @@ -110,8 +110,8 @@ Proof. intros s1; elim s1; simpl in |- *; auto. intros s2 n; rewrite plus_comm; simpl in |- *; auto. intros a s1' Rec s2 n; case n; simpl in |- *; auto. -generalize (Rec s2 0); simpl in |- *; auto. -intros n0; rewrite <- Plus.plus_Snm_nSm; auto. +generalize (Rec s2 0); simpl in |- *; auto. intros. +rewrite <- Plus.plus_Snm_nSm; auto. Qed. (** *** Substrings *) -- cgit v1.2.3