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 /parsing | |
| 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 'parsing')
| -rw-r--r-- | parsing/g_vernac.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4 index fc0a4c8c31..3bd190bb8a 100644 --- a/parsing/g_vernac.ml4 +++ b/parsing/g_vernac.ml4 @@ -420,7 +420,7 @@ GEXTEND Gram [ [ "("; a = simple_assum_coe; ")" -> a ] ] ; simple_assum_coe: - [ [ idl = LIST1 identref; oc = of_type_with_opt_coercion; c = lconstr -> + [ [ idl = LIST1 pidentref; oc = of_type_with_opt_coercion; c = lconstr -> (not (Option.is_empty oc),(idl,c)) ] ] ; |