diff options
| author | Pierre-Marie Pédrot | 2015-10-07 15:08:27 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-08 13:05:14 +0200 |
| commit | 33d153a01f2814c6e5486c07257667254b91fa0c (patch) | |
| tree | cc335368f42b3a879522cbf4888f842a138a6f18 /lib/cThread.ml | |
| parent | 479d45e679e8486c65b77f2ddfa8718c24778a75 (diff) | |
Axioms now support the universe binding syntax.
We artificially restrict the syntax though, because it is unclear of
what the semantics of several axioms in a row is, in particular about the
resolution of remaining evars.
Diffstat (limited to 'lib/cThread.ml')
0 files changed, 0 insertions, 0 deletions