aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2013-09-27Removing a bunch of generic equalities.ppedrot
2013-09-19Made the filename of compiled files explicit, i.e. add a ./ prefixppedrot
2013-09-19Get rid of the uses of deprecated OCaml elements (still remaining compatible ...xclerc
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-09-18Removing almost all new_untyped_evar, and a bunch of Evd.add.ppedrot
2013-09-13STM pretty printer should never failgareuselesinge
2013-09-13fix STM feeback on running jobsgareuselesinge
2013-09-12Unplugging Autoinstance. The code is still here if someone wishesppedrot
2013-09-12CoqIDE: show number of proofs being checked in backgroundgareuselesinge
2013-09-12Unknown commands starting a proof were not setting the proof mode.gareuselesinge
2013-09-12Remove outdated commentgareuselesinge
2013-09-12VernacList handling was lost in STM mergegareuselesinge
2013-09-10Temporary fix of emacs mode for ProofGeneralletouzey
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-30summary for ML modules made correctgareuselesinge
2013-08-30Make the jopin-document button wait for slaves to terminategareuselesinge
2013-08-30When PG is used as interface behave as before STMgareuselesinge
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-30Stm: if slave process dies badly go back to local lazy evaluationgareuselesinge
2013-08-30-coq-slaves: close_on_exec + correct argument passinggareuselesinge
2013-08-28Fixing bug #3083.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-20Fix STM: Module Import may change the parsergareuselesinge
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Himsg : strict 80-column indentationletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-19Modulification and removing of structural equality in VCS.ppedrot
2013-08-12Fixing potentially misused Errors.push.ppedrot
2013-08-11Mutual proofs cannot be delegatedgareuselesinge
2013-08-10Small typosppedrot
2013-08-10Lemmas ending with Defined cannot be delegated to slavesgareuselesinge
2013-08-09Fix batch compilation of scripts with Admitted proofs (in a section)gareuselesinge
2013-08-09fix batch compilation of scripts containing Admittedgareuselesinge
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
2013-08-08Support Proof Generalgareuselesinge
2013-08-08Coqide ported to STMgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-06Added more flags choice in desambiguating printer. The code isppedrot
2013-08-05Tentative fix for bug #2961. When we have to print two terms thatppedrot
2013-08-04Fixing #2846: Uncaught exception Reduction.NotArity.ppedrot
2013-08-04Removing useless casts between arrays and lists.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 20:17:35 +0000