diff options
| -rw-r--r-- | toplevel/metasyntax.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 2ccd27acb..92208e304 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -982,7 +982,7 @@ let make_interpretation_type isrec = function | NtnInternTypeConstr when isrec -> NtnTypeConstrList | NtnInternTypeConstr | NtnInternTypeIdent -> NtnTypeConstr | NtnInternTypeBinder when isrec -> NtnTypeBinderList - | NtnInternTypeBinder -> error "Type not allowed in recursive notation." + | NtnInternTypeBinder -> error "Type binder is only for use in recursive notations for binders." let make_interpretation_vars recvars allvars = let eq_subscope (sc1, l1) (sc2, l2) = |