diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-27 11:16:15 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-27 11:16:15 +0000 |
| commit | e961ace331ec961dcec0e2525d7b9142d04b5154 (patch) | |
| tree | 08ffca7a4fdb28b5a79f3409d8478deecb099c3d /theories/Strings | |
| parent | fc10282837971f8f0648841d944dd64b11d3a3db (diff) | |
- 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
Diffstat (limited to 'theories/Strings')
| -rw-r--r-- | theories/Strings/String.v | 4 |
1 files changed, 2 insertions, 2 deletions
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 *) |