diff options
| author | herbelin | 2008-06-11 11:18:41 +0000 |
|---|---|---|
| committer | herbelin | 2008-06-11 11:18:41 +0000 |
| commit | ba61b1c136505c901c23f6a83cae6d29cedcd96c (patch) | |
| tree | 5fdf8bf7b8b678204291bd57f8413a1f5680ce6c /pretyping/typeclasses_errors.ml | |
| parent | f69af1fe44d2a1ff7260147ca643a4f4981379cd (diff) | |
Plutôt que de reposer sur le vernacexpr pour détecter les débuts de
buts, on se base sur les informations de Pfedit (comme le fait Pierre
Courtieu). Permet d'être plus robuste sur les extensions de syntaxe
ouvrant des buts, style Function.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11101 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/typeclasses_errors.ml')
0 files changed, 0 insertions, 0 deletions