diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-25 16:30:40 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-25 16:30:40 +0000 |
| commit | c65747ba8e36672b7a4828f46e459ef920608acb (patch) | |
| tree | 3801d93fece89cf5a56c8fdad0d8f80cae619099 /contrib/extraction/table.mli | |
| parent | 95477bc8750375047d0c86dfbfda41ed221cac3c (diff) | |
cleanup table.ml + erreur si Extraction Inline sous section
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3284 85f007b7-540e-0410-9357-904b9bb8a0f7
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 c951116ba..4a21619ac 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 |