diff options
| author | ppedrot | 2013-11-09 07:08:59 +0000 |
|---|---|---|
| committer | ppedrot | 2013-11-09 07:08:59 +0000 |
| commit | 36e41e7581c86214a9f0f97436eb96a75b640834 (patch) | |
| tree | 2c99a4b163e976272c7931d0889611d8c13a15ae /kernel/type_errors.ml | |
| 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 'kernel/type_errors.ml')
0 files changed, 0 insertions, 0 deletions