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 /intf | |
| 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 'intf')
| -rw-r--r-- | intf/vernacexpr.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/intf/vernacexpr.mli b/intf/vernacexpr.mli index fd6e1c6ae1..f89f076b5f 100644 --- a/intf/vernacexpr.mli +++ b/intf/vernacexpr.mli @@ -314,7 +314,7 @@ type vernac_expr = | VernacEndProof of proof_end | VernacExactProof of constr_expr | VernacAssumption of (locality option * assumption_object_kind) * - inline * simple_binder with_coercion list + inline * (plident list * constr_expr) with_coercion list | VernacInductive of private_flag * inductive_flag * (inductive_expr * decl_notation list) list | VernacFixpoint of locality option * (fixpoint_expr * decl_notation list) list |