proof-general - Emacs plugins for proof management systems

Age	Commit message (Collapse)	Author
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).
2013-07-10	Fixing #478 + reverting partially the fix of #476 (Instance cannot be ↵	Pierre Courtieu
	indented by default).
2013-07-10	Fixing #476 (bis). Adding Fixpoint as a goal starter.	Pierre Courtieu

2013-07-10	Fixing #476. Adding more keywords for indentation like Lemma.	Pierre Courtieu

2013-07-10	Fixing #475. the "=>" ptoken just before "exists" should be the ltac	Pierre Courtieu
	"=>" most of the time.
2013-07-08	Fixing again bug #466. With a bbetter solution.	Pierre Courtieu
	Not using "b o f" token anymore.
2013-07-06	Fixing #474. & is now an declared operator. I need something better to	Pierre Courtieu
	capture any operator and give it a (configurable?) precedence.
2013-07-06	Fixing #473. Now all token finishing by <symbol><dot> is considered an	Pierre Courtieu
	end of command, except if exactly <dot><dot>
2013-07-05	Fixing #466. Indent. bug when illformed commment at file beginning.	Pierre Courtieu
	Nasty bug due to smie fallback to backward-sexp when finding an unknown token, namely the token "", which happens when reaching the bof. Had to add a specific token for b o f.
2013-05-30	Adding some more standard utf8 symbols to indentation operator. We	Pierre Courtieu
	really need some "operator" recognition here.
2013-05-29	Fixing a minor bug in indetation (exists is tactic and a quantifier).	Pierre Courtieu

2012-09-25	Fixed indentation in presence of "dot friends" like :?. etc.	Pierre Courtieu

2012-09-06	Fixed a bug with function name "eval" (end of).	Pierre Courtieu

2012-09-06	Fixed a bug with function name "eval".	Pierre Courtieu

2012-08-24	Fixed an error when smie not present in the system.	Pierre Courtieu

2012-07-24	Fixing compilation. Still need to verify some smie stuff on different ↵	Pierre Courtieu
	versions of emacs.
2012-07-09	Fixed a small bug in indentation + added new commands for queries with	Pierre Courtieu
	Printing Implicit and Printing All flags.
2012-07-07	Debugged coq indentation.	Pierre Courtieu

2012-07-06	More fixes in coq indentation (2).	Pierre Courtieu

2012-07-06	More fixes in coq indentation.	Pierre Courtieu

2012-07-05	Indentation debugging for coq.	Pierre Courtieu

2012-07-05	Code cleaning.	Pierre Courtieu

2012-07-05	Fixed some indentation details for Coq.	Pierre Courtieu

2012-07-03	Fixed some indentation bugs.	Pierre Courtieu

2012-06-28	Fixed some small bugs in coq indentation.	Pierre Courtieu

2012-06-28	Complete rework of the indentation mechanism using smie. The first	Pierre Courtieu
	version of smie indentation code was a good first try but this one is much faster and cleaner. All desambiguations are done in the lexers, it is still a bit slow on large proofs. Some bugs remain to be fixed.