Context Navigation

Timeline

8:58 PM Ticket #483 (ltac: and constr: should not affect indentation) created by coquser: This indentation (done by TAB) is wrong: […]

7:16 PM Ticket #482 ([lazymatch] should be highlighted and indented like [match]) created by coquser: Currently, it causes the branches to be deindented, and does not match …

10:31 PM Ticket #452 (Some Isabelle options enabled but not active) closed by Makarius: fixed

12:18 PM Ticket #467 (The "Time (tactic)." vernacular command no longer displays timings ...) closed by coquser: fixed: The menu entries are fixed now, such that, when you select "Time …
11:12 AM Ticket #481 (proof-set-value does not handle errors in :eval forms of defpacustom) created by coquser: Hi, proof-set-value evaluates the :eval form when a defpacustom …

1:49 PM Ticket #480 ([match]es sometimes screw up indentation) created by coquser: Here is some code poorly indented by TAB: […] The second …

9:48 PM Ticket #479 ([intros ??.] messes up following indentation) created by coquser: […] Should not be indented this way. (Adding a space between the …

5:01 PM Ticket #478 ([Proof <body term>.] messes up following indentation) closed by courtieu: fixed: Thanks, should be fixed in cvs. Proof. Proof with foo. are goal …
4:03 PM Ticket #477 ([Proposition] is not highlighted like [Lemma]) closed by courtieu: fixed: Thanks. Fixed.
4:03 PM Ticket #476 ([Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have ...) closed by courtieu: fixed: Thanks! Fixed.
12:45 PM Ticket #475 ([exists] tactic causes improper indentation) closed by courtieu: fixed: Thanks again for the report. Fixed.
12:54 AM Ticket #478 ([Proof <body term>.] messes up following indentation) created by coquser: The following is some code indented with TAB: […]
12:51 AM Ticket #477 ([Proposition] is not highlighted like [Lemma]) created by coquser: In my version of emacs + PG, Instance, Lemma, etc all get …
12:50 AM Ticket #476 ([Goal], [Proposition], [Intance], [Fixpoint], [Corollary] do not have ...) created by coquser: PG indents as follows […] And similarly for Proposition, …
12:46 AM Ticket #475 ([exists] tactic causes improper indentation) created by coquser: Here is some code indented by TAB: […]

9:16 PM Ticket #474 (Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning ...) closed by courtieu: fixed: Quick fix for &. But I still need a way to deal with all operators, …
3:50 PM Ticket #473 (Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]) closed by courtieu: fixed: Fixed. Thanks for the bug report. I decided to consider all tokens …

4:26 PM Ticket #474 (Indentation screwed up in sigT notations ("{ _ : _ & _ }") spanning ...) created by coquser: Here's some code formatted by TAB in emacs PG: […] The …
4:16 PM Ticket #473 (Indentation screwed up by "/." (not by "/ .") in, e.g., [Arguments foo /.]) created by coquser: The following two blocks of code have been indented by highlighting …
3:01 PM Ticket #466 (parentheses in comments should not affect indentation level of ...) closed by courtieu: fixed: Fixed in cvs. Nasty bug due to smie fallback to smie-backward-sexp …

Note: See TracTimeline for information about the timeline view.