From 51976c9f2157953f794ed1efcd68403a8545d346 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 9 Aug 2017 13:58:59 +0200 Subject: A bit of miscellaneous code documentation around notations. --- vernac/metasyntax.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'vernac/metasyntax.ml') 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) = -- cgit v1.2.3