aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/syntax_def.mli
diff options
context:
space:
mode:
Diffstat (limited to 'interp/syntax_def.mli')
-rw-r--r--interp/syntax_def.mli2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/syntax_def.mli b/interp/syntax_def.mli
index 3ba78e91d..747f7b9da 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -21,7 +21,7 @@ open Libnames
type syndef_interpretation = (identifier * subscopes) list * aconstr
-val declare_syntactic_definition : bool -> identifier -> bool ->
+val declare_syntactic_definition : bool -> identifier -> bool ->
syndef_interpretation -> unit
val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation