aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-09-07Change syntax of Hint Resolve to actually accept user-given priorities.msozeau
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-09-05Optimizing some evar_maps manipulation. In particular, using a [map] insteadppedrot
2013-09-05Documentation of Evd.ppedrot
2013-09-05Cleaning up of Evd. Extruding the tower of modules used to define evar_maps.ppedrot
2013-09-04More robust argument setter in CoqIDE. It does not crash anymore on badppedrot
2013-09-03Fixing some tests from the test-suite.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-09-03Some cleanup in Autoppedrot
2013-09-02Removing more association lists in Constrintern.ppedrot
2013-09-02* test-suite/success/Unicode_utf8:regisgia
2013-09-02* lib/Unicode:regisgia
2013-09-02* parsing/Lexer: Cosmetics.regisgia
2013-09-02* configure: Remove trailing space.regisgia
2013-08-30summary for ML modules made correctgareuselesinge
2013-08-30add "Print Ring" and "Print Field" vernacular commandsgareuselesinge
2013-08-30Make the jopin-document button wait for slaves to terminategareuselesinge
2013-08-30Fixing the code of field_simplify_eq.amahboub
2013-08-30When PG is used as interface behave as before STMgareuselesinge
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-30recdef: restore old semantics (pre STM)gareuselesinge
2013-08-30Fix typo in error messagegareuselesinge
2013-08-30safe Conv_oracle state for type checkinggareuselesinge
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-30Remove Obj.magic from safe typinggareuselesinge
2013-08-30Trickyer test for Paral-ITPgareuselesinge
2013-08-28Fixing bug #3083.ppedrot
2013-08-28Removing some lone List.assoc & List.mem in lib.ppedrot
2013-08-25Removing association lists in Reductionops. Btw, defining the dual of theppedrot
2013-08-25Actually using the domain function for maps.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-25Replacing lists by sets in clear tactic.ppedrot
2013-08-23Adding dynamic value printing to votour through a registering mechanism.ppedrot
2013-08-23Fix computation of discharged hyps for inductive types forgetting the conclus...msozeau
2013-08-23Updating documentation of the ring/field tactics.amahboub
2013-08-23Fixing an incompleteness of the ring/field tacticsamahboub
2013-08-22Correcting misplaced Proof command.amahboub
2013-08-22Fixing a significant efficiency leak in the code of the field tactic.amahboub
2013-08-22Nicer code concerning dirpaths and modpath around Libletouzey
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-22micromega: remove empty file CheckerMakerletouzey
2013-08-22More complete hashcons : lists (dirpath), arrays (constr)letouzey
2013-08-22Change in vo format : digest aren't Marshalled anymoreletouzey
2013-08-22Field_theory : faster and nicer proofs + nice notations.letouzey
2013-08-22Ring_polynom : shorter proof for Psub_okletouzey
2013-08-20Partial revert of r16711letouzey
2013-08-20Fixing votourppedrot
2013-08-20Fix compilation of dev/printres.cmagareuselesinge
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 07:52:23 +0000