aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Fixing bug #3083.Gravatar ppedrot2013-08-28
* Removing some lone List.assoc & List.mem in lib.Gravatar ppedrot2013-08-28
* Removing association lists in Reductionops. Btw, defining the dual of theGravatar ppedrot2013-08-25
* Actually using the domain function for maps.Gravatar ppedrot2013-08-25
* Added a more efficient way to recover the domain of a map.Gravatar ppedrot2013-08-25
* Replacing lists by sets in clear tactic.Gravatar ppedrot2013-08-25
* Adding dynamic value printing to votour through a registering mechanism.Gravatar ppedrot2013-08-23
* Fix computation of discharged hyps for inductive types forgetting the conclus...Gravatar msozeau2013-08-23
* Updating documentation of the ring/field tactics.Gravatar amahboub2013-08-23
* Fixing an incompleteness of the ring/field tacticsGravatar amahboub2013-08-23
* Correcting misplaced Proof command.Gravatar amahboub2013-08-22
* Fixing a significant efficiency leak in the code of the field tactic.Gravatar amahboub2013-08-22
* Nicer code concerning dirpaths and modpath around LibGravatar letouzey2013-08-22
* Misc changes around coqtop.ml :Gravatar letouzey2013-08-22
* Less "Coq" strings everywhereGravatar letouzey2013-08-22
* micromega: remove empty file CheckerMakerGravatar letouzey2013-08-22
* More complete hashcons : lists (dirpath), arrays (constr)Gravatar letouzey2013-08-22
* Change in vo format : digest aren't Marshalled anymoreGravatar letouzey2013-08-22
* Field_theory : faster and nicer proofs + nice notations.Gravatar letouzey2013-08-22
* Ring_polynom : shorter proof for Psub_okGravatar letouzey2013-08-22
* Partial revert of r16711Gravatar letouzey2013-08-20
* Fixing votourGravatar ppedrot2013-08-20
* Fix compilation of dev/printres.cmaGravatar gareuselesinge2013-08-20
* Fix compilation of coqcheckGravatar gareuselesinge2013-08-20
* CoqIDE: fixed detection of edits in the locked zoneGravatar gareuselesinge2013-08-20
* Fix STM: Module Import may change the parserGravatar gareuselesinge2013-08-20
* Universe counters on slaves are in sync with masterGravatar gareuselesinge2013-08-20
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Declareops + Modops : more clever substitutionsGravatar letouzey2013-08-20
* Himsg : strict 80-column indentationGravatar letouzey2013-08-20
* Mod_typing : code cleanupGravatar letouzey2013-08-20
* Safe_typing code refactoringGravatar letouzey2013-08-20
* Attempt to restore hash-consing of opaque termsGravatar letouzey2013-08-20
* Repair coqcheck : constant_body constraints are also futureGravatar letouzey2013-08-20
* Modulification and removing of structural equality in Stateid.Gravatar ppedrot2013-08-19
* Modulification and removing of structural equality in VCS.Gravatar ppedrot2013-08-19
* Cleanup code in term_typingGravatar gareuselesinge2013-08-19
* abstract+Defined: create opaque sub proofs (as pre-ParalITP)Gravatar gareuselesinge2013-08-19
* Tooltips can be augmented with custom widgets, still not clickableGravatar gareuselesinge2013-08-19
* Setting tooltip font monospace.Gravatar ppedrot2013-08-12
* Fixing potentially misused Errors.push.Gravatar ppedrot2013-08-12
* Automatic backtracking if locked zone is editedGravatar gareuselesinge2013-08-11
* Mutual proofs cannot be delegatedGravatar gareuselesinge2013-08-11
* Printing any backtrace in debug mode, not only anomalies.Gravatar ppedrot2013-08-10
* Small typosGravatar ppedrot2013-08-10
* Lemmas ending with Defined cannot be delegated to slavesGravatar gareuselesinge2013-08-10
* Adding the processed tag to comments in CoqIDE.Gravatar ppedrot2013-08-09
* Fix batch compilation of scripts with Admitted proofs (in a section)Gravatar gareuselesinge2013-08-09
* checker validation fixed w.r.t. FuturesGravatar gareuselesinge2013-08-09
* checker validation made a bit more verboseGravatar gareuselesinge2013-08-09
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 17:47:55 +0000