diff options
| author | Gaëtan Gilbert | 2019-08-08 23:13:39 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-08-08 23:15:30 +0200 |
| commit | 4b81a2269919ad47c03aab5a1e578c34f3cc6ed1 (patch) | |
| tree | 9f820adc77f47b2ce8c3f4632e18a52946fac8b1 /vernac/comFixpoint.ml | |
| parent | 9fdeb13166af29bfc6ec1e1930f1932ddc9f1cd4 (diff) | |
Emit Feedback.AddedAxiom in Declare instead of higher layers
This lets us remove the passing around of "status" in comassumption
and generally makes highlighting axiom adding lines in coqide more
reliable as there's no need for per-command code.
If a command adds multiple axioms it will emit AddedAxiom multiple
times, this doesn't seem to be a problem though.
We may wonder if "Fail Fail Axiom" should be highlighted as
"Axiom" (both before and after this commit it is).
Diffstat (limited to 'vernac/comFixpoint.ml')
| -rw-r--r-- | vernac/comFixpoint.ml | 13 |
1 files changed, 2 insertions, 11 deletions
diff --git a/vernac/comFixpoint.ml b/vernac/comFixpoint.ml index 74c9bc2886..b6843eab33 100644 --- a/vernac/comFixpoint.ml +++ b/vernac/comFixpoint.ml @@ -323,11 +323,6 @@ let adjust_rec_order ~structonly binders rec_order = in Option.map (extract_decreasing_argument ~structonly) rec_order -let check_safe () = - let open Declarations in - let flags = Environ.typing_flags (Global.env ()) in - flags.check_universes && flags.check_guarded - let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = let fixl = List.map (fun fix -> Vernacexpr.{ fix @@ -339,13 +334,11 @@ let do_fixpoint_common (fixl : Vernacexpr.fixpoint_expr list) = let do_fixpoint_interactive ~scope ~poly l : Lemmas.t = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~indexes:possible_indexes ~scope ~poly fix ntns in - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_fixpoint ~scope ~poly l = let fixl, ntns, fix, possible_indexes = do_fixpoint_common l in - declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + declare_fixpoint_generic ~indexes:possible_indexes ~scope ~poly fix ntns let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = let fixl = List.map (fun fix -> {fix with Vernacexpr.rec_order = None}) fixl in @@ -355,10 +348,8 @@ let do_cofixpoint_common (fixl : Vernacexpr.cofixpoint_expr list) = let do_cofixpoint_interactive ~scope ~poly l = let cofix, ntns = do_cofixpoint_common l in let lemma = declare_fixpoint_interactive_generic ~scope ~poly cofix ntns in - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else (); lemma let do_cofixpoint ~scope ~poly l = let cofix, ntns = do_cofixpoint_common l in - declare_fixpoint_generic ~scope ~poly cofix ntns; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + declare_fixpoint_generic ~scope ~poly cofix ntns |