diff options
Diffstat (limited to 'toplevel/metasyntax.mli')
| -rw-r--r-- | toplevel/metasyntax.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/toplevel/metasyntax.mli b/toplevel/metasyntax.mli index 216d03381..44e7133e2 100644 --- a/toplevel/metasyntax.mli +++ b/toplevel/metasyntax.mli @@ -43,7 +43,7 @@ val add_notation_interpretation : (** Add a notation interpretation for supporting the "where" clause *) -val set_notation_for_interpretation : Constrintern.full_internalization_env -> +val set_notation_for_interpretation : Constrintern.internalization_env -> (lstring * constr_expr * scope_name option) -> unit (** Add only the parsing/printing rule of a notation *) |