diff options
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index 3da01fe090..e97a0a41e2 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -26,7 +26,10 @@ val list_of_implicits : implicits -> int list val declare_var_implicits : section_path -> unit val declare_constant_implicits : section_path -> unit -val declare_inductive_implicits : section_path -> unit +val declare_mib_implicits : section_path -> unit + +val declare_implicits : global_reference -> unit +val declare_manual_implicits : global_reference -> int list -> unit (*s Access to already computed implicits. *) @@ -41,7 +44,7 @@ val constant_implicits_list : section_path -> int list val implicits_of_var : section_path -> int list val is_implicit_constant : section_path -> bool -val is_implicit_inductive_definition : section_path -> bool +val is_implicit_inductive_definition : inductive_path -> bool val is_implicit_var : section_path -> bool val implicits_of_global : global_reference -> int list |