diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 20:24:54 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-04-13 20:24:54 +0000 |
| commit | a0717999ef44b284fd761ee86bf5f2c25feccba0 (patch) | |
| tree | 02553e9d02c00cb65b3e099e962509958d1922dd /plugins/extraction/table.mli | |
| parent | 60bc3cbe72083f4fa1aa759914936e4fa3d6b42e (diff) | |
Extraction: opaque terms are not traversed anymore by default
In signatures, opaque terms are always seen as parameters.
In implementations, a flag Set/Unset Extraction AccessOpaque
allows to customize things:
- Set : opacity is ignored (this is the old behavior)
- Unset : opaque terms are extracted as axioms (default now)
Some warnings are anyway emitted when extraction encounters
informative opaque terms.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13999 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/extraction/table.mli')
| -rw-r--r-- | plugins/extraction/table.mli | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/plugins/extraction/table.mli b/plugins/extraction/table.mli index 97c28b154..dc07349ca 100644 --- a/plugins/extraction/table.mli +++ b/plugins/extraction/table.mli @@ -19,7 +19,7 @@ val safe_basename_of_global : global_reference -> identifier (*s Warning and Error messages. *) val warning_axioms : unit -> unit -val warning_opaques : unit -> unit +val warning_opaques : bool -> unit val warning_both_mod_and_cst : qualid -> module_path -> global_reference -> unit val warning_id : string -> unit @@ -89,6 +89,10 @@ val remove_opaque : global_reference -> unit val reset_tables : unit -> unit +(*s AccessOpaque parameter *) + +val access_opaque : unit -> bool + (*s AutoInline parameter *) val auto_inline : unit -> bool |