diff options
Diffstat (limited to 'contrib/extraction/table.mli')
| -rw-r--r-- | contrib/extraction/table.mli | 15 |
1 files changed, 10 insertions, 5 deletions
diff --git a/contrib/extraction/table.mli b/contrib/extraction/table.mli index c951116ba0..4a21619ac2 100644 --- a/contrib/extraction/table.mli +++ b/contrib/extraction/table.mli @@ -8,10 +8,19 @@ (*i $Id$ i*) -open Vernacinterp open Names open Libnames +(*s Warning and Error messages. *) + +val error_section : unit -> 'a + +val error_axiom_scheme : kernel_name -> 'a + +val error_axiom : kernel_name -> 'a + +val warning_axiom : kernel_name -> unit + (*s AutoInline parameter *) val auto_inline : unit -> bool @@ -49,12 +58,8 @@ val ml_type_extractions : unit -> (global_reference * string) list val ml_term_extractions : unit -> (global_reference * string) list - - (*s Extraction commands. *) -open Util - val extraction_language : lang -> unit val extraction_inline : bool -> reference list -> unit |