diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 32 |
1 files changed, 12 insertions, 20 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 8c9fdf37d..35494d3d2 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -175,14 +175,10 @@ let add_info_axiom r = info_axioms := Refset'.add r !info_axioms let remove_info_axiom r = info_axioms := Refset'.remove r !info_axioms let add_log_axiom r = log_axioms := Refset'.add r !log_axioms -let opaques_ok = ref Refset'.empty -let opaques_ko = ref Refset'.empty -let init_opaques () = opaques_ok := Refset'.empty; opaques_ko := Refset'.empty -let add_opaque_ok r = opaques_ok := Refset'.add r !opaques_ok -let add_opaque_ko r = opaques_ko := Refset'.add r !opaques_ko -let remove_opaque r = - opaques_ok := Refset'.remove r !opaques_ok; - opaques_ko := Refset'.remove r !opaques_ko +let opaques = ref Refset'.empty +let init_opaques () = opaques := Refset'.empty +let add_opaque r = opaques := Refset'.add r !opaques +let remove_opaque r = opaques := Refset'.remove r !opaques (*s Extraction modes: modular or monolithic, library or minimal ? @@ -263,23 +259,19 @@ let warning_axioms () = str "Having invalid logical axiom in the environment when extracting" ++ spc () ++ str "may lead to incorrect or non-terminating ML terms." ++ fnl ()) - end + end; + if !Flags.load_proofs = Flags.Dont && info_axioms@log_axioms <> [] then + msg_warning + (str "Some of these axioms might by due to option -dont-load-proofs.") let warning_opaques () = - let opaques_ok = Refset'.elements !opaques_ok in - if opaques_ok = [] then () + let opaques = Refset'.elements !opaques in + if opaques = [] then () else msg_warning (str "Extraction is accessing the body of the following opaque constants:" - ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ok) + ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques) ++ str "." ++ fnl () - ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ()); - let opaques_ko = Refset'.elements !opaques_ko in - if opaques_ko = [] then () - else msg_warning - (str "Extraction cannot access the body of the following opaque constants:" - ++ hov 1 (spc () ++ prlist_with_sep spc safe_pr_global opaques_ko) - ++ fnl () ++ str "due to option -dont-load-proofs. " - ++ str "These constants are treated as axioms." ++ fnl ()) + ++ str "Be careful if using option -dont-load-proofs later." ++ fnl ()) let warning_both_mod_and_cst q mp r = msg_warning |