diff options
Diffstat (limited to 'contrib/extraction/table.mli')
| -rw-r--r-- | contrib/extraction/table.mli | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 413fa8ed3..e4169a9bf 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -62,9 +62,10 @@ val lookup_ind : kernel_name -> ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool -val add_record : kernel_name -> global_reference list -> unit +val add_record : kernel_name -> int -> global_reference list -> unit val find_projections : kernel_name -> global_reference list val is_projection : global_reference -> bool +val projection_arity : global_reference -> int val add_aliases : module_path -> module_path -> unit val long_mp : module_path -> module_path |