diff options
Diffstat (limited to 'pretyping/syntax_def.ml')
| -rw-r--r-- | pretyping/syntax_def.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/syntax_def.ml b/pretyping/syntax_def.ml index 736a2be67..00ed971c1 100644 --- a/pretyping/syntax_def.ml +++ b/pretyping/syntax_def.ml @@ -31,7 +31,7 @@ let (in_syntax_constant, out_syntax_constant) = cache_function = cache_syntax_constant; load_function = (fun _ -> ()); open_function = cache_syntax_constant; - specification_function = (fun x -> x) } + export_function = (fun x -> Some x) } in declare_object ("SYNTAXCONSTANT", od) |