| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix a type error hidden until recent emacs. |  Pierre Courtieu | 2016-06-23 |
| | | |||
| * | Fix #47. | Pierre Courtieu | 2016-03-09 |
| | | | | | There are many other issued with coq-smie-forward-token. | ||
| * | Fixing a small glitch in indentation. | Pierre Courtieu | 2016-03-09 |
| | | | | | | if a "; tactic" is not at the end of its line, (hanging) then it should not act on indetation of next line. | ||
| * | Fix #63 (efficiency pb in indentation). | Pierre Courtieu | 2016-03-09 |
| | | |||
| * | Avoiding useless computation in indentation code. | Pierre Courtieu | 2016-03-08 |
| | | |||
| * | Add uconstr to the (ltac constr) list in SMIE |  Clément Pit--Claudel | 2016-02-27 |
| | | |||
| * | Fix a typo: s/coq-modulestart-proofstart/coq-indent-proofstart/ | Clément Pit--Claudel | 2016-02-27 |
| | | |||
| * | Add a :safe predicate to indentation variables | Clément Pit--Claudel | 2016-02-27 |
| | | | | | This is useful if people want to set them project-locally. | ||
| * | Fix #29 + indentation glitch + regexp refactoring. | Pierre Courtieu | 2016-01-14 |
| | | |||
| * | Fixing indentation of ";". | Pierre Courtieu | 2016-01-08 |
| | | | | | | Local/Global Tactic Notation | ||
| * | indentation of ";" more accurate. | Pierre Courtieu | 2016-01-08 |
| | | | | | | Now detecting if the ; is inside a parenthesized tactic (--> no spurious indentation). | ||
| * | Fixing outdenting in ";" indetation. | Pierre Courtieu | 2016-01-08 |
| | | |||
| * | Trying to indent ";" differently inside Ltac defs. | Pierre Courtieu | 2016-01-08 |
| | | | | | | | | This only works when the command starts with "Ltac". Ideally we would like to switch to no indentation of ";" each time the ";" is the child of something else that ends a command "." or bullets). | ||
| * | Fixed indentation of ";" tactical. | Pierre Courtieu | 2016-01-07 |
| | | |||
| * | Adding uset preference coq-indent-semicolon-tactical. | Pierre Courtieu | 2016-01-06 |
| | | | | | | | | | | Some people prefer ";" tactical to be non indented, in particular in Ltac definitions. Setting this variable to 0 (2 by default) does it. You can still have some indentation by putting ; at beginning of lines: tac1 ; tac2 ; tac3. | ||
| * | Fixed #15 + more speedup of indentation. | Pierre Courtieu | 2015-12-05 |
| | | | | | | Experimenting on more regexp and less adhoc searching in the smie lexer. In particular the regexp for bullet seems now capture only real bullets. | ||
| * | Speeding up indentation code (smie lexer). | Pierre Courtieu | 2015-11-30 |
| | | |||
| * | Fixes #486 with an option. |  Pierre Courtieu | 2015-05-07 |
| | | |||
| * | Yet another half fix of smie lexer. | Pierre Courtieu | 2015-05-07 |
| | | | | | || is either a boolean operator or a tactical. | ||
| * | Trying to prepare indentation cleaning... | Pierre Courtieu | 2015-04-03 |
| | | |||
| * | Fixed smie code for ";" + added || in grammar. | Pierre Courtieu | 2015-03-31 |
| | | | | | | Actually || and + are overloaded and I don"t see how to deambiguate them. Indetation may be buggy until I found away. | ||
| * | Fixed a small bug in indentation. | Pierre Courtieu | 2015-03-27 |
| | | |||
| * | Fixed indetation of tryif then else. | Pierre Courtieu | 2015-03-24 |
| | | |||
| * | Fixed lazymatch and multimatch indentation/highlighting. | Pierre Courtieu | 2015-03-23 |
| | | |||
| * | Customization variables for modules, section and proof indentation. | Pierre Courtieu | 2015-03-05 |
| | | |||
| * | Fixed Proof end/start detection on Proof using ... | Pierre Courtieu | 2015-03-04 |
| | | | | | | Was making scripting confused. P. | ||
| * | changed default indentation of match's cases. | Pierre Courtieu | 2015-01-14 |
| | | |||
| * | failed and commented attempt at improving indentation of records. | Pierre Courtieu | 2015-01-09 |
| | | |||
| * | Fixing indentation of pending curly braces. | Pierre Courtieu | 2015-01-05 |
| | | |||
| * | Fix compile on 23.x |  David Aspinall | 2015-01-05 |
| | | |||
| * | trying to indent pending forall in the expected way | Pierre Courtieu | 2015-01-05 |
| | | |||
| * | fixed indentation (lexing of 'with') + made local coq-load-path. | Pierre Courtieu | 2014-12-30 |
| | | |||
| * | fixed a bug in command parsing for coq, due to recent changes. | Pierre Courtieu | 2014-12-24 |
| | | |||
| * | typo in indentation cod, found after testing coq/ex/indent.v. | Pierre Courtieu | 2014-12-24 |
| | | |||
| * | fixing a small pb in indentation of arrow (->). Not perfect. | Pierre Courtieu | 2014-12-24 |
| | | |||
| * | fixed the use of >= 24.4 function string-suffix-p. | Pierre Courtieu | 2014-12-24 |
| | | |||
| * | Supporting more bullets (coq 8.5), like ++ or ++++. | Pierre Courtieu | 2014-12-23 |
| | | |||
| * | * coq/coq-smie.el: Fix precedence of 'else'. |  Stefan Monnier | 2014-06-06 |
| | | |||
| * | * coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition. | Stefan Monnier | 2014-06-04 |
| | | | | | | (coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=". | ||
| * | Rename coq-smie-lexer.el to coq-smie.el. | Stefan Monnier | 2014-06-03 |
 |
index : proof-general | |
| Emacs interface for proof assistants |
| aboutsummaryrefslogtreecommitdiffhomepage |