| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix most doc issues raised by (checkdoc) |  Erik Martin-Dorel | 2018-08-23 |
| | | |||
| * | Support the Variant vernacular |  Tej Chajed | 2018-08-17 |
| | | | | | | Syntactically looks much like an Inductive, though it is non-recursive so "where" (mutual recursion) is not supported. | ||
| * | Update copyright messages and improve the header of elisp files. | Erik Martin-Dorel | 2018-02-21 |
| | | |||
| * | Experimental fix for #220. |  Pierre Courtieu | 2018-01-15 |
| | | |||
| * | Limited extensibility of smie token detection. | Pierre Courtieu | 2017-10-26 |
| | | |||
| * | Fixing #183. | Pierre Courtieu | 2017-05-23 |
| | | |||
| * | Fix #176. | Pierre Courtieu | 2017-04-19 |
| | | | | | | The code uses several token searcher and the wrong one was called somewhere. | ||
| * | Fixing #147 and #91 + others indentation bugs. | Pierre Courtieu | 2017-01-26 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | While fixing these I discovered several flaws in indentation (what a suprise). The probem is the following: since we don't have a precise grammar of tactics, smie often decides that the parent of a sub-part of a tactic is the previous command instead of the current tacic. Typical example (fixed now but in general): foo. apply bar with bar'. Since "apply ... bar'" is considered as one leaf of the grammar, it is considered to be a child of the previous dot. . /\ / \ foo apply...bar' Therefore indentation of "with" wants to align with parent "." and hence with "foo". Basically we should try to define a much more precise grammar of complex tactics (with with, as, using etc) in order to fix the problem. Of course this has the drawback of making impossible to support user tactic notations. | ||
| * | add second argument to looking-back, required in emacs25 |  Hendrik Tews | 2016-12-31 |
| | | |||
| * | 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 |