aboutsummaryrefslogtreecommitdiffhomepage
path: root/proofs
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-28 10:55:30 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2016-06-29 09:32:41 +0200
commit8e07227c5853de78eaed4577eefe908fb84507c0 (patch)
treeb74780ac62cf49d9edc18dd846e96e79f6e24bf6 /proofs
parentc5e8224aa77194552b0e4c36f3bb8d40eb27a12b (diff)
A new infrastructure for warnings.
On the user side, coqtop and coqc take a list of warning names or categories after -w. No prefix means activate the warning, a "-" prefix means deactivate it, and "+" means turn the warning into an error. Special categories include "all", and "default" which contains the warnings enabled by default. We also provide a vernacular Set Warnings which takes the same flags as argument. Note that coqc now prints warnings. The name and category of a warning are printed with the warning itself. On the developer side, Feedback.msg_warning is still accessible, but the recommended way to print a warning is in two steps: 1) create it by: let warn_my_warning = CWarnings.create ~name:"my-warning" ~category:"my-category" (fun args -> Pp.strbrk ...) 2) print it by: warn_my_warning args
Diffstat (limited to 'proofs')
-rw-r--r--proofs/redexpr.ml16
1 files changed, 13 insertions, 3 deletions
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 13b5848a3..ee5591521 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -29,10 +29,15 @@ let cbv_vm env sigma c =
error "vm_compute does not support existential variables.";
Vnorm.cbv_vm env c ctyp
+let warn_native_compute_disabled =
+ CWarnings.create ~name:"native-compute-disabled" ~category:"native-compiler"
+ (fun () ->
+ strbrk "native_compute disabled at configure time; falling back to vm_compute.")
+
let cbv_native env sigma c =
if Coq_config.no_native_compiler then
- let () = Feedback.msg_warning (str "native_compute disabled at configure time; falling back to vm_compute.") in
- cbv_vm env sigma c
+ (warn_native_compute_disabled ();
+ cbv_vm env sigma c)
else
let ctyp = Retyping.get_type_of env sigma c in
Nativenorm.native_norm env sigma c ctyp
@@ -209,6 +214,11 @@ let contextualize f g = function
e_red (contextually b (l,c) (fun _ -> h))
| None -> e_red g
+let warn_simpl_unfolding_modifiers =
+ CWarnings.create ~name:"simpl-unfolding-modifiers" ~category:"tactics"
+ (fun () ->
+ Pp.strbrk "The legacy simpl ignores constant unfolding modifiers.")
+
let reduction_of_red_expr env =
let make_flag = make_flag env in
let rec reduction_of_red_expr = function
@@ -221,7 +231,7 @@ let reduction_of_red_expr env =
let am = if !simplIsCbn then strong_cbn (make_flag f) else simpl in
let () =
if not (!simplIsCbn || List.is_empty f.rConst) then
- Feedback.msg_warning (Pp.strbrk "The legacy simpl does not deal with delta flags.") in
+ warn_simpl_unfolding_modifiers () in
(contextualize (if head_style then whd_am else am) am o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
| Cbn f ->