aboutsummaryrefslogtreecommitdiff
path: root/plugins/syntax/string_notation.ml
diff options
context:
space:
mode:
authorGaëtan Gilbert2019-08-08 23:13:39 +0200
committerGaëtan Gilbert2019-08-08 23:15:30 +0200
commit4b81a2269919ad47c03aab5a1e578c34f3cc6ed1 (patch)
tree9f820adc77f47b2ce8c3f4632e18a52946fac8b1 /plugins/syntax/string_notation.ml
parent9fdeb13166af29bfc6ec1e1930f1932ddc9f1cd4 (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 'plugins/syntax/string_notation.ml')
0 files changed, 0 insertions, 0 deletions