aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2014-01-18unicode tokens for \<open>, \<close>, \<newline>;Makarius Wenzel
2013-10-11Set version tag for new release.David Aspinall
2013-07-22Added comment.Pierre Courtieu
2013-07-22Added some information on coq project file in doc.Pierre Courtieu
2013-07-22Fixing coq project file parsing + moved project options.Pierre Courtieu
2013-07-17fix type of coq-project-filenameHendrik Tews
2013-07-17disable and protect coq-hide-additional-subgoals-switch for coq-time-commandsHendrik Tews
2013-07-17Fix image nameDavid Aspinall
2013-07-17Set version tag for new release.David Aspinall
2013-07-17update TAGSHendrik Tews
2013-07-17fix ProofGeneral.texi for infoHendrik Tews
2013-07-11add two Coq faq entries and improve some otherHendrik Tews
2013-07-11remove backup fileHendrik Tews
2013-07-11fix typo and compilationHendrik Tews
2013-07-11fix two bugs in parallel compilation for CoqHendrik Tews
2013-07-11Fixing a big bug in coq project file management.Pierre Courtieu
file and directory name were not adapted to where the current file is inside the directory structure. Now the absolute names are build.
2013-07-11Fixing another bug in indentation concerning "where". Actually therePierre Courtieu
are other uses of "where (declaring notation for records that I did no test).
2013-07-10Fixing #478 + reverting partially the fix of #476 (Instance cannot be ↵Pierre Courtieu
indented by default).
2013-07-10Fixing #476 (bis). Adding Fixpoint as a goal starter.Pierre Courtieu
2013-07-10Fixing #477. Adding Proposition as a goal-starter keyword.Pierre Courtieu
2013-07-10Fixing #476. Adding more keywords for indentation like Lemma.Pierre Courtieu
2013-07-10Fixing #475. the "=>" ptoken just before "exists" should be the ltacPierre Courtieu
"=>" most of the time.
2013-07-09Fixed interaction between file variables and coq project file + faq.Pierre Courtieu
2013-07-08Updating coq/faqPierre Courtieu
2013-07-08Fixing again bug #466. With a bbetter solution.Pierre Courtieu
Not using "b o f" token anymore.
2013-07-06Fixing #474. & is now an declared operator. I need something better toPierre Courtieu
capture any operator and give it a (configurable?) precedence.
2013-07-06Fixing #473. Now all token finishing by <symbol><dot> is considered anPierre Courtieu
end of command, except if exactly <dot><dot>
2013-07-05Updating pg documentation about new feature coq project file.Pierre Courtieu
2013-07-05Fixing #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-07-05more appropriate URL;Makarius Wenzel
2013-07-05Set version tag for new release.David Aspinall
2013-07-05Document Make checkDavid Aspinall
2013-07-04Fixing a compilation warning for a ml4pg function in coq.el.Pierre Courtieu
2013-07-04Fixing undeclared variables for compilation.Pierre Courtieu
2013-07-02Added faq for coq pg.Pierre Courtieu
2013-07-02Fixing coq project file mechanism.Pierre Courtieu
2013-06-21Added an entry to CHANGEs about coq project fields.Pierre Courtieu
2013-06-19Adding support for coq project file for setting coqdoc args.Pierre Courtieu
second attempt, seems better (cleaner code).
2013-06-19Adding support for coq project file for setting coqdoc args.Pierre Courtieu
First attempt, seems ok.
2013-05-31Authors of ML4PGjoheras
2013-05-31Removing files from ML4PG folderjoheras
2013-05-31Removing ML4PG files from coq folder.joheras
2013-05-31Removing ML4PG files from coq folder.joheras
2013-05-31Inclusion of ML4PG in coq.el file.joheras
2013-05-31Moving ML4PG from coq directory to contrib directory.joheras
2013-05-31Remove link in tar file.David Aspinall
2013-05-31*** empty log message ***joheras
2013-05-31Removing hidden files of ML4PG.joheras
2013-05-31Removing hidden files from ML4PG.joheras
2013-05-31ML4PG modificationjoheras