index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
...
*
* configure: Remove trailing space.
regisgia
2013-09-02
*
summary for ML modules made correct
gareuselesinge
2013-08-30
*
add "Print Ring" and "Print Field" vernacular commands
gareuselesinge
2013-08-30
*
Make the jopin-document button wait for slaves to terminate
gareuselesinge
2013-08-30
*
Fixing the code of field_simplify_eq.
amahboub
2013-08-30
*
When PG is used as interface behave as before STM
gareuselesinge
2013-08-30
*
ind_tables: properly handling side effects
gareuselesinge
2013-08-30
*
recdef: restore old semantics (pre STM)
gareuselesinge
2013-08-30
*
Fix typo in error message
gareuselesinge
2013-08-30
*
safe Conv_oracle state for type checking
gareuselesinge
2013-08-30
*
Stm: if slave process dies badly go back to local lazy evaluation
gareuselesinge
2013-08-30
*
-coq-slaves: close_on_exec + correct argument passing
gareuselesinge
2013-08-30
*
Remove Obj.magic from safe typing
gareuselesinge
2013-08-30
*
Trickyer test for Paral-ITP
gareuselesinge
2013-08-30
*
Fixing bug #3083.
ppedrot
2013-08-28
*
Removing some lone List.assoc & List.mem in lib.
ppedrot
2013-08-28
*
Removing association lists in Reductionops. Btw, defining the dual of the
ppedrot
2013-08-25
*
Actually using the domain function for maps.
ppedrot
2013-08-25
*
Added a more efficient way to recover the domain of a map.
ppedrot
2013-08-25
*
Replacing lists by sets in clear tactic.
ppedrot
2013-08-25
*
Adding dynamic value printing to votour through a registering mechanism.
ppedrot
2013-08-23
*
Fix computation of discharged hyps for inductive types forgetting the conclus...
msozeau
2013-08-23
*
Updating documentation of the ring/field tactics.
amahboub
2013-08-23
*
Fixing an incompleteness of the ring/field tactics
amahboub
2013-08-23
*
Correcting misplaced Proof command.
amahboub
2013-08-22
*
Fixing a significant efficiency leak in the code of the field tactic.
amahboub
2013-08-22
*
Nicer code concerning dirpaths and modpath around Lib
letouzey
2013-08-22
*
Misc changes around coqtop.ml :
letouzey
2013-08-22
*
Less "Coq" strings everywhere
letouzey
2013-08-22
*
micromega: remove empty file CheckerMaker
letouzey
2013-08-22
*
More complete hashcons : lists (dirpath), arrays (constr)
letouzey
2013-08-22
*
Change in vo format : digest aren't Marshalled anymore
letouzey
2013-08-22
*
Field_theory : faster and nicer proofs + nice notations.
letouzey
2013-08-22
*
Ring_polynom : shorter proof for Psub_ok
letouzey
2013-08-22
*
Partial revert of r16711
letouzey
2013-08-20
*
Fixing votour
ppedrot
2013-08-20
*
Fix compilation of dev/printres.cma
gareuselesinge
2013-08-20
*
Fix compilation of coqcheck
gareuselesinge
2013-08-20
*
CoqIDE: fixed detection of edits in the locked zone
gareuselesinge
2013-08-20
*
Fix STM: Module Import may change the parser
gareuselesinge
2013-08-20
*
Universe counters on slaves are in sync with master
gareuselesinge
2013-08-20
*
Declarations.mli: reorganization of modular structures
letouzey
2013-08-20
*
Declareops + Modops : more clever substitutions
letouzey
2013-08-20
*
Himsg : strict 80-column indentation
letouzey
2013-08-20
*
Mod_typing : code cleanup
letouzey
2013-08-20
*
Safe_typing code refactoring
letouzey
2013-08-20
*
Attempt to restore hash-consing of opaque terms
letouzey
2013-08-20
*
Repair coqcheck : constant_body constraints are also future
letouzey
2013-08-20
*
Modulification and removing of structural equality in Stateid.
ppedrot
2013-08-19
*
Modulification and removing of structural equality in VCS.
ppedrot
2013-08-19
[prev]
[next]