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 747f7b9da..b4da6dd7a 100644
--- a/interp/syntax_def.mli
+++ b/interp/syntax_def.mli
@@ -24,4 +24,4 @@ type syndef_interpretation = (identifier * subscopes) list * aconstr
val declare_syntactic_definition : bool -> identifier -> bool ->
syndef_interpretation -> unit
-val search_syntactic_definition : loc -> kernel_name -> syndef_interpretation
+val search_syntactic_definition : kernel_name -> syndef_interpretation