| Age | Commit message (Expand) | Author |
|---|
| 2011-07-16 | Added a characterization of unique existence. | herbelin |
| 2011-07-15 | A correct error message for an unknown field in a record definition | pboutill |
| 2011-07-11 | Makefiles generated by coq_makefile can build %.cmx?a from %.mllib | pboutill |
| 2011-07-11 | Stores bullet stack on locally at the level of focuses rather than globally i... | aspiwack |
| 2011-07-08 | Coqide: undo comments (Second part of r14268) | pboutill |
| 2011-07-07 | coq_makefile logical path ending with '.' are correctly convert to physical path | pboutill |
| 2011-07-07 | coq_makefile bug fix 2405: cmxs are now made from cmx files | pboutill |
| 2011-07-07 | coq_makefile documentation in Refman and -h | pboutill |
| 2011-07-07 | coq_makefile doesn't complain anymore when a dir is both -I and -R | pboutill |
| 2011-07-07 | Bug 2217: In coqide, a comment alone is now a sentence that isn't send to coq | pboutill |
| 2011-07-07 | Coqide understand { and } | pboutill |
| 2011-07-07 | default install location under cygwin is the unix default | pboutill |
| 2011-07-07 | bug 2423: consider "" as the empty prefix | barras |
| 2011-07-07 | fixed coqchk usage and man page + added option -coqlib | barras |
| 2011-07-06 | Fixed bullets so that they would play well with { }. | aspiwack |
| 2011-07-05 | Adding a new syntax for BeginSubproof and EndSubproof, namely { and }. | courtieu |
| 2011-07-04 | Set Extraction KeepSingleton: an option for not decapsulating singleton types | letouzey |
| 2011-07-04 | StrictOrder marked explicitly to be in Prop | letouzey |
| 2011-07-04 | Extraction: in haskell, __ may have any type, no need to unsafeCoerce it | letouzey |
| 2011-07-04 | Extraction: in haskell, type signatures for __ and unsafeCoerce (fix #2552) | letouzey |
| 2011-07-04 | Extraction: forbid Prop-polymorphism of inductives when extracting to Ocaml | letouzey |
| 2011-07-04 | doc/stdlib: Update the list of ZArith files | letouzey |
| 2011-07-01 | Some cleanup of Zcomplements | letouzey |
| 2011-07-01 | Cleanup of files related with power over Z. | letouzey |
| 2011-06-30 | Fix compilation error | msozeau |
| 2011-06-30 | Keep obligation source information in Program | msozeau |
| 2011-06-30 | Cleanup in SpecViaZ | letouzey |
| 2011-06-30 | Cleanup of Ndigits | letouzey |
| 2011-06-29 | update of Micromega doc | fbesson |
| 2011-06-28 | Deletion of useless Zdigits_def | letouzey |
| 2011-06-28 | Deletion of useless Zlog_def | letouzey |
| 2011-06-28 | Deletion of useless Zsqrt_def | letouzey |
| 2011-06-28 | Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_def | letouzey |
| 2011-06-28 | Some cleanup of Wf_Z.v | letouzey |
| 2011-06-28 | improved tactic names | fbesson |
| 2011-06-27 | Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base) | letouzey |
| 2011-06-27 | Znumtheory: a correct version of a compatibility Zdivide_intro | letouzey |
| 2011-06-24 | Clean-up of Znumtheory, deletion of Zgcd_def | letouzey |
| 2011-06-24 | Numbers: a particular case of div_unique | letouzey |
| 2011-06-24 | Numbers: change definition of divide (compat with Znumtheory) | letouzey |
| 2011-06-23 | cleanup of Zsgn | letouzey |
| 2011-06-23 | cleanup of Zmin and Zmax | letouzey |
| 2011-06-23 | Some more cleanup of Zorder | letouzey |
| 2011-06-22 | fix bug 2510: xml test is in the summary if it fails | pboutill |
| 2011-06-21 | Follow-up concerning eqb / ltb / leb comparisons | letouzey |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-06-20 | Some migration of results from BinInt to Numbers | letouzey |
| 2011-06-20 | Zcompare.destr_zcompare subsumed by case Z.compare_spec | letouzey |
| 2011-06-20 | Clean-up of Zcompare and Zorder | letouzey |
| 2011-06-20 | Arithemtic: more concerning compare, eqb, leb, ltb | letouzey |
