coq - The formal proof system

Age	Commit message (Expand)	Author
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-28	Fixing bug #3083.	ppedrot
2013-08-28	Removing some lone List.assoc & List.mem in lib.	ppedrot
2013-08-25	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-23	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-22	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-20	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-19	Modulification and removing of structural equality in Stateid.	ppedrot
2013-08-19	Modulification and removing of structural equality in VCS.	ppedrot
2013-08-19	Cleanup code in term_typing	gareuselesinge
2013-08-19	abstract+Defined: create opaque sub proofs (as pre-ParalITP)	gareuselesinge
2013-08-19	Tooltips can be augmented with custom widgets, still not clickable	gareuselesinge
2013-08-12	Setting tooltip font monospace.	ppedrot
2013-08-12	Fixing potentially misused Errors.push.	ppedrot
2013-08-11	Automatic backtracking if locked zone is edited	gareuselesinge
2013-08-11	Mutual proofs cannot be delegated	gareuselesinge
2013-08-10	Printing any backtrace in debug mode, not only anomalies.	ppedrot
2013-08-10	Small typos	ppedrot
2013-08-10	Lemmas ending with Defined cannot be delegated to slaves	gareuselesinge
2013-08-09	Adding the processed tag to comments in CoqIDE.	ppedrot