diff options
Diffstat (limited to 'plugins/extraction/extraction.ml')
| -rw-r--r-- | plugins/extraction/extraction.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml index a6a9838ae8..5c67c33b6a 100644 --- a/plugins/extraction/extraction.ml +++ b/plugins/extraction/extraction.ml @@ -110,7 +110,7 @@ let rec type_scheme_nb_args env c = if is_info_scheme env t then n+1 else n | _ -> 0 -let _ = register_type_scheme_nb_args type_scheme_nb_args +let _ = Hook.set type_scheme_nb_args_hook type_scheme_nb_args (*s [type_sign_vl] does the same, plus a type var list. *) |