diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-09 13:58:59 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | 51976c9f2157953f794ed1efcd68403a8545d346 (patch) | |
| tree | 612cc59179d2d16d5bb552f31f0abda92e50dd23 /vernac | |
| parent | 6901f720c6115c8eec1343846641a5c8453c3268 (diff) | |
A bit of miscellaneous code documentation around notations.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/metasyntax.ml b/vernac/metasyntax.ml index 09eb0503d..462f6215a 100644 --- a/vernac/metasyntax.ml +++ b/vernac/metasyntax.ml @@ -956,7 +956,7 @@ let make_interpretation_type isrec isonlybinding = function | NtnInternTypeConstr | NtnInternTypeIdent -> if isonlybinding then NtnTypeOnlyBinder else NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.") + | NtnInternTypeBinder -> user_err Pp.(str "Type binder is only for use in recursive notations for binders.") let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = |