diff options
| author | Emilio Jesus Gallego Arias | 2020-03-09 01:51:37 -0400 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2020-03-25 06:03:42 -0400 |
| commit | 09d6197bd11ed4a323b335118ae749d7caefeb55 (patch) | |
| tree | 361c538ea06c34e8e1dc99309fa62816bb759e01 /vernac/declareDef.mli | |
| parent | a0296d51711cdd42f201b9d0e937266984a20944 (diff) | |
[proof] [mutual] Factorize notation declaration.
Diffstat (limited to 'vernac/declareDef.mli')
| -rw-r--r-- | vernac/declareDef.mli | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/vernac/declareDef.mli b/vernac/declareDef.mli index 38a2da4261..971f924c6c 100644 --- a/vernac/declareDef.mli +++ b/vernac/declareDef.mli @@ -67,6 +67,7 @@ val declare_mutually_recursive -> scope:locality -> kind:Decls.logical_kind -> ubind:UnivNames.universe_binders + -> ntns:Vernacexpr.decl_notation list -> Names.variable list -> Constr.constr list -> Constr.types list |