diff options
| author | Pierre-Marie Pédrot | 2016-03-31 23:35:38 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-31 23:35:38 +0200 |
| commit | 8d272227e4a4b4829678bfb6ecc84673bc47eeb7 (patch) | |
| tree | 3d20d152bda6bc687177b857a07096191af099fe /test-suite | |
| parent | c0aefc5323cb4393297adcaffd2967ab93ab815e (diff) | |
| parent | bacba3d3ec0dd54d210bdf5045bc7e193c904b3c (diff) | |
Providing an API to access the parsing engine summary in a first-class way.
Instead of hardwiring a few special cases in Egramcoq, we allow the grammar
state to contain arbitrary data structures. This permits to extend the parsing
engine while retaining the synchronization with the global state, e.g. for use
in plugins.
Diffstat (limited to 'test-suite')
| -rw-r--r-- | test-suite/bugs/closed/1850.v | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test-suite/bugs/closed/1850.v b/test-suite/bugs/closed/1850.v new file mode 100644 index 0000000000..26b48093b7 --- /dev/null +++ b/test-suite/bugs/closed/1850.v @@ -0,0 +1,4 @@ +Parameter P : Type -> Type -> Type. +Notation "e |= t --> v" := (P e t v) (at level 100, t at level 54). +Fail Check (nat |= nat --> nat). + |