proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
2020-10-16	Fix #514 + support for named goal selector.	Pierre Courtieu
	It was hard to separate this too fixes (same regexps).
2020-01-19	Generic monadic indentation + specifically ext-lib / Compcert + doc.	Pierre Courtieu
	This a generalization of PR#451 proposed by @Chobbes. Since these syntax are not completely universal (and not builtin in coq), the idea is to make the syntax customizable, especially to make it possible to disable it. NOTE: to make the Compcert syntax supported I had to refine the smie lexer so that the ";" token was emitted as a fllback instead of "; tactic". NOTE2: I had to make the coq-user-token and coq-monadic-tokens be tested ON THE RESULT of smie-coq-backward-token.
2019-06-17	fixing with inductive indentation.	Pierre Courtieu

2017-05-23	Fixing #183.	Pierre Courtieu

2017-01-26	Fixing #147 and #91 + others indentation bugs.	Pierre Courtieu
	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.
2015-03-23	Fixed lazymatch and multimatch indentation/highlighting.	Pierre Courtieu

2015-01-05	Fixing indentation of pending curly braces.	Pierre Courtieu

2015-01-05	trying to indent pending forall in the expected way	Pierre Courtieu

2014-12-30	fixed indentation (lexing of 'with') + made local coq-load-path.	Pierre Courtieu

2014-12-24	fixed a bug in command parsing for coq, due to recent changes.	Pierre Courtieu

2014-06-06	* coq/coq-smie.el: Fix precedence of 'else'.	Stefan Monnier

2014-06-04	* coq-smie.el (coq-smie-.-deambiguate): Proofs don't start with a definition.	Stefan Monnier
	(coq-smie-backward-token): Don't burp at EOB. (coq-smie-rules): Indent top-level ":" like ":=".
2014-06-03	Rename coq-smie-lexer.el to coq-smie.el.	Stefan Monnier

2013-07-11	Fixing another bug in indentation concerning "where". Actually there	Pierre Courtieu
	are other uses of "where (declaring notation for records that I did no test).
2012-07-10	Fixed incorrect syntax of previous commit.	Pierre Courtieu

2012-06-08	Indentation is a bit more accurate.	Pierre Courtieu

2012-06-07	Fix indentation of dependent match clauses (as ... in ... return ...).	Pierre Courtieu
	+ bug fixes.
2012-06-04	One more fix for indentation.	Pierre Courtieu

2012-06-03	Fix a bug of indentation.	Pierre Courtieu

2012-02-10	Fixed an ineficiency in comment detection.	Pierre Courtieu

2011-07-08	Fixing the scripting of new subproof script parenthesizing ({ and }).	Pierre Courtieu

2011-07-01	Some more sample indentation patterns added.	Pierre Courtieu

2011-06-17	oops, undo last commit.	Pierre Courtieu

2011-06-10	Fix trac #410.	Pierre Courtieu

2011-06-08	Added one indentation example.	Pierre Courtieu

2011-06-04	Updated the old code for indentation, in case Stefan cannot finish the	Pierre Courtieu
	new one for the release. Added also support for an experimental syntax modification: { .. } is a new syntax for Beginsubproof. ... EndSubproof. There a also few minor behavior changes. The code has changed a lot though.
2010-09-09	Fixed small bugs in indentation.	Pierre Courtieu