diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-09 07:08:59 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-11-09 07:08:59 +0000 |
| commit | 36e41e7581c86214a9f0f97436eb96a75b640834 (patch) | |
| tree | 2c99a4b163e976272c7931d0889611d8c13a15ae /tactics/tactics.mllib | |
| parent | 485ab2c54051b3c9127477956002956971d41e3b (diff) | |
Revert the previous commit. It broke Coq compilation.
Tactics notation interpretation was messed up because of the use of
identical keys for different notations. All my tentative fixes were
unsuccessful, so better blankly revert the commit for now.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@17078 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'tactics/tactics.mllib')
| -rw-r--r-- | tactics/tactics.mllib | 1 |
1 files changed, 0 insertions, 1 deletions
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index f1227c234..7b91665ad 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -15,7 +15,6 @@ Equality Contradiction Inv Leminv -Tacenv Tacsubst Taccoerce Tacintern |