From a0717999ef44b284fd761ee86bf5f2c25feccba0 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 13 Apr 2011 20:24:54 +0000
Subject: 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
---
 plugins/extraction/extract_env.ml | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'plugins/extraction/extract_env.ml')

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index c4dce1c7b4..1263055665 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -487,6 +487,10 @@ let init modular library =
   reset ();
   if modular && lang () = Scheme then error_scheme ()
 
+let warns () =
+  warning_opaques (access_opaque ());
+  warning_axioms ()
+
 (* From a list of [reference], let's retrieve whether they correspond
    to modules or [global_reference]. Warn the user if both is possible. *)
 
@@ -513,8 +517,7 @@ let full_extr f (refs,mps) =
   init false false;
   List.iter (fun mp -> if is_modfile mp then error_MPfile_as_mod mp true) mps;
   let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
-  warning_opaques ();
-  warning_axioms ();
+  warns ();
   print_structure_to_file (mono_filename f) false struc;
   reset ()
 
@@ -527,8 +530,7 @@ let separate_extraction lr =
   init true false;
   let refs,mps = locate_ref lr in
   let struc = optimize_struct (refs,mps) (mono_environment refs mps) in
-  warning_opaques ();
-  warning_axioms ();
+  warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	print_structure_to_file (module_filename mp) false [e]
@@ -546,8 +548,7 @@ let simple_extraction r = match locate_ref [r] with
       init false false;
       let struc = optimize_struct ([r],[]) (mono_environment [r] []) in
       let d = get_decl_in_structure r struc in
-      warning_opaques ();
-      warning_axioms ();
+      warns ();
       if is_custom r then msgnl (str "(** User defined extraction *)");
       print_one_decl struc (modpath_of_r r) d;
       reset ()
@@ -573,8 +574,7 @@ let extraction_library is_rec m =
   in
   let struc = List.fold_left select [] l in
   let struc = optimize_struct ([],[]) struc in
-  warning_opaques ();
-  warning_axioms ();
+  warns ();
   let print = function
     | (MPfile dir as mp, sel) as e ->
 	let dry = not is_rec && dir <> dir_m in
-- 
cgit v1.2.3