aboutsummaryrefslogtreecommitdiffhomepage
path: root/vernac
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-08-09 13:58:59 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2018-02-20 10:03:04 +0100
commit51976c9f2157953f794ed1efcd68403a8545d346 (patch)
tree612cc59179d2d16d5bb552f31f0abda92e50dd23 /vernac
parent6901f720c6115c8eec1343846641a5c8453c3268 (diff)
A bit of miscellaneous code documentation around notations.
Diffstat (limited to 'vernac')
-rw-r--r--vernac/metasyntax.ml2
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) =