aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-08-20CoqIDE: fixed detection of edits in the locked zonegareuselesinge
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-20Declareops + Modops : more clever substitutionsletouzey
2013-08-20Himsg : strict 80-column indentationletouzey
2013-08-20Mod_typing : code cleanupletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-20Attempt to restore hash-consing of opaque termsletouzey
2013-08-20Repair coqcheck : constant_body constraints are also futureletouzey
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-19Modulification and removing of structural equality in VCS.ppedrot
2013-08-19Cleanup code in term_typinggareuselesinge
2013-08-19abstract+Defined: create opaque sub proofs (as pre-ParalITP)gareuselesinge
2013-08-19Tooltips can be augmented with custom widgets, still not clickablegareuselesinge
2013-08-12Setting tooltip font monospace.ppedrot
2013-08-12Fixing potentially misused Errors.push.ppedrot
2013-08-11Automatic backtracking if locked zone is editedgareuselesinge
2013-08-11Mutual proofs cannot be delegatedgareuselesinge
2013-08-10Printing any backtrace in debug mode, not only anomalies.ppedrot
2013-08-10Small typosppedrot
2013-08-10Lemmas ending with Defined cannot be delegated to slavesgareuselesinge
2013-08-09Adding the processed tag to comments in CoqIDE.ppedrot
2013-08-09Fix batch compilation of scripts with Admitted proofs (in a section)gareuselesinge
2013-08-09checker validation fixed w.r.t. Futuresgareuselesinge
2013-08-09checker validation made a bit more verbosegareuselesinge
2013-08-09fix batch compilation of scripts containing Admittedgareuselesinge
2013-08-09state_id data typegareuselesinge
2013-08-08Gtk check_buttons do have a labelgareuselesinge
2013-08-08calling interp by hand is forbiddengareuselesinge
2013-08-08Add a (very minimal) Proof General mode to CoqIDEgareuselesinge
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-08Test for Paral-ITPgareuselesinge
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-08Fix testsuite so that it works with STMgareuselesinge
2013-08-08Manual fixed w.r.t. STMgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
2013-08-08Vcs data structure (Git inspired builder for Dag)gareuselesinge
2013-08-08Dag data structuregareuselesinge
2013-08-08Searchable stack data structuregareuselesinge
2013-08-08Future library to represent pure computationsgareuselesinge
2013-08-08Fixing a warning in CoqIDE compilation.ppedrot
2013-08-08Small fix in IStream interface.ppedrot
2013-08-07Removing association lists in Constrintern.ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 05:33:45 +0000