diff options
Diffstat (limited to 'contrib/extraction/table.mli')
| -rw-r--r-- | contrib/extraction/table.mli | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index 6be869e59..cc793b1a1 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -11,6 +11,7 @@ open Names open Libnames open Miniml +open Declarations val id_of_global : global_reference -> identifier @@ -55,8 +56,8 @@ val lookup_term : constant -> ml_decl val add_type : constant -> ml_schema -> unit val lookup_type : constant -> ml_schema -val add_ind : kernel_name -> ml_ind -> unit -val lookup_ind : kernel_name -> ml_ind +val add_ind : kernel_name -> mutual_inductive_body -> ml_ind -> unit +val lookup_ind : kernel_name -> mutual_inductive_body * ml_ind val add_recursors : Environ.env -> kernel_name -> unit val is_recursor : global_reference -> bool |