aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2012-10-30rename entities in coq-seq-compileHendrik Tews
2012-10-30move some more material into coq-compile-commonHendrik Tews
2012-10-30update TAGSHendrik Tews
2012-10-30move general part of compilation into coq-compile-common.elHendrik Tews
2012-10-30move coq compilation into coq/coq-seq-compile.elHendrik Tews
2012-10-19Set version tag for new release.David Aspinall
2012-10-19Updates for PG 4.3David Aspinall
2012-10-19Set version tag for new release.David Aspinall
2012-10-03"as" insertion on a region.Pierre Courtieu
2012-10-03Fixed auto-insert-as stuff + fix compiling problems.Pierre Courtieu
2012-10-02Made 'as' automatic insertion a togglable feature (not finished) (2).Pierre Courtieu
2012-10-02Made 'as' automatic insertion a togglable feature. Not finished.Pierre Courtieu
2012-10-02Fixed 'as' close automatic insertion.Pierre Courtieu
2012-10-01Fixed the coq-insert-as feature. Will only work on coq svn trunk forPierre Courtieu
now. coq-8.4 not compatible.
2012-09-25Fixed #419: coq synchronized variables are not anymore in the settingsPierre Courtieu
menu, they are in option menu that only issues commands to the prover and do not try to keep track of the values of the variables.
2012-09-25Fixed a bug in three windows mode.Pierre Courtieu
2012-09-25Added a menu to set the 3 windows layout.Pierre Courtieu
2012-09-25Fixed indentation in presence of "dot friends" like :?. etc.Pierre Courtieu
2012-09-24Fixed docstring of proof-layout-windows for two columns mode.Was notPierre Courtieu
up-to-date.
2012-09-24Fixing a docstring.Pierre Courtieu
2012-09-24Completing the possible layouts of proof-layout-windows (added the 3Pierre Courtieu
columns mode).
2012-09-21Fixing a bad interaction between one unicode token and electricPierre Courtieu
terminator.
2012-09-19Small fix in holes code.Pierre Courtieu
2012-09-14Set version tag for new release.David Aspinall
2012-09-14proof-shell-process-connection-type: try using pipes by default in Emacs 24,David Aspinall
to avoid Trac #453: http://proofgeneral.inf.ed.ac.uk/trac/ticket/453
2012-09-14Updated.David Aspinall
2012-09-14coq-remove-trailing-dot: Fix accidental dynamic binding so it compilesDavid Aspinall
2012-09-14no braces and bullets for prooftreeHendrik Tews
2012-09-14adjust proof-tree regexp for focused subgoalsHendrik Tews
2012-09-12treat #450 by requiring that proofs are started with ProofHendrik Tews
2012-09-07Fix of the last commit.Pierre Courtieu
2012-09-07Added one point + details to CHANGES.Pierre Courtieu
2012-09-07Fix a bug that was letting "." in a wrong syntax category.Pierre Courtieu
2012-09-07Cleaning code and comments.Pierre Courtieu
2012-09-07Fixed a bug with coq symbol detection at point. Now dot notation.are supported.Pierre Courtieu
2012-09-06Fixed a bug with function name "eval" (end of).Pierre Courtieu
2012-09-06Fixed a bug with function name "eval".Pierre Courtieu
2012-09-05Fixed double hit terminator. Now it is disabled by default, andPierre Courtieu
enabling it disables electric-terminator and vice-versa. In case both are non nil at the same time, then electric teminator has priority. If people like it we may propose this to other modes than coq. + fixed window layout policy.
2012-09-04Set version tag for new release.David Aspinall
2012-09-04Fix compile for Emacs 24David Aspinall
2012-09-04Disable HOL Light support for release versionDavid Aspinall
2012-09-02Remove functions defined for Emacs 22 compatibilityDavid Aspinall
2012-09-02Repair operation with compiled code. Fails with interpreter, see Trac #445David Aspinall
2012-09-02Remove ref to file parsingcheck-412.v missing from CVS, so "make ↵David Aspinall
coq.autotest" runs again
2012-09-02Fix headerDavid Aspinall
2012-09-02Set version tag for new release.David Aspinall
2012-08-31 Three windows mode is back as the default mode.Pierre Courtieu
2012-08-31Changed the behaviour of proof-layout-windows. Now it follows thePierre Courtieu
'horizontal 'vertical 'smart policy.
2012-08-31Fixing a bug happening in coq when three win mode on and scriptingPierre Courtieu
starts on a buffer. The response buffer was hiding the scripting buffer. NOTE: this is not a bug correction. The bug is still there but proof-layout-windows is called to work it around.
2012-08-31Setting nil by default the option to create resp and goals bufferPierre Courtieu
immediately when opening a file.
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 04:44:57 +0000