diff options
Diffstat (limited to 'vernac/metasyntax.ml')
| -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) = |