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 /theories/Reals/Rcomplete.v | |
| 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 'theories/Reals/Rcomplete.v')
0 files changed, 0 insertions, 0 deletions