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/comProgramFixpoint.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/comProgramFixpoint.ml')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 16 |
1 files changed, 3 insertions, 13 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index c6e68effd7..3497e6369f 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -292,7 +292,7 @@ let do_program_recursive ~scope ~poly fixkind fixl = let ntns = List.map_append (fun { Vernacexpr.notations } -> notations ) fixl in Obligations.add_mutual_definitions defs ~poly ~scope ~kind ~univdecl:pl ctx ntns fixkind -let do_program_fixpoint ~scope ~poly l = +let do_fixpoint ~scope ~poly l = let g = List.map (fun { Vernacexpr.rec_order } -> rec_order) l in match g, l with | [Some { CAst.v = CWfRec (n,r) }], @@ -322,19 +322,9 @@ let do_program_fixpoint ~scope ~poly l = do_program_recursive ~scope ~poly fixkind l | _, _ -> - user_err ~hdr:"do_program_fixpoint" + user_err ~hdr:"do_fixpoint" (str "Well-founded fixpoints not allowed in mutually recursive blocks") -let check_safe () = - let open Declarations in - let flags = Environ.typing_flags (Global.env ()) in - flags.check_universes && flags.check_guarded - -let do_fixpoint ~scope ~poly l = - do_program_fixpoint ~scope ~poly l; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () - let do_cofixpoint ~scope ~poly fixl = let fixl = List.map (fun fix -> { fix with Vernacexpr.rec_order = None }) fixl in - do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl; - if not (check_safe ()) then Feedback.feedback Feedback.AddedAxiom else () + do_program_recursive ~scope ~poly DeclareObl.IsCoFixpoint fixl |