diff options
| author | Arnaud Spiwack | 2015-09-25 09:39:56 +0200 |
|---|---|---|
| committer | Arnaud Spiwack | 2015-09-25 10:41:41 +0200 |
| commit | 0b20282c49253aea4429384467b75a5bdb1f8ba4 (patch) | |
| tree | 8da9a32a2c04604d9af6df9f275a80980af95dea | |
| parent | 9f4e67a7c9f22ca853e76f4837a276a6111bf159 (diff) | |
Declare assumptions of well-founded definitions as unsafe.
So that fixpoints and cofixpoints which are assumed to be total are highlighted in yellow in Coqide, for instance.
| -rw-r--r-- | toplevel/command.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml index ac46b439cf..c6d67b13ac 100644 --- a/toplevel/command.ml +++ b/toplevel/command.ml @@ -1209,7 +1209,8 @@ let do_fixpoint ~chkguard local poly l = let fix = interp_fixpoint fixl ntns in let possible_indexes = List.map compute_possible_guardness_evidences (pi3 fix) in - declare_fixpoint ~chkguard local poly fix possible_indexes ntns + declare_fixpoint ~chkguard local poly fix possible_indexes ntns; + if not chkguard then Pp.feedback Feedback.AddedAxiom else () let do_cofixpoint ~chkguard local poly l = let fixl,ntns = extract_cofixpoint_components l in @@ -1217,4 +1218,5 @@ let do_cofixpoint ~chkguard local poly l = do_program_recursive local poly Obligations.IsCoFixpoint fixl ntns else let cofix = interp_cofixpoint fixl ntns in - declare_cofixpoint ~chkguard local poly cofix ntns + declare_cofixpoint ~chkguard local poly cofix ntns; + if not chkguard then Pp.feedback Feedback.AddedAxiom else () |