| Age | Commit message (Expand) | Author |
|---|
| 2011-07-22 | Allow custom targets without commands specified | pboutill |
| 2011-07-22 | For the beauty of tail recursion, a new list_addn | pboutill |
| 2011-07-20 | Fix typo in coqmktop help | glondu |
| 2011-07-18 | Fixed a "feature" of "inversion" and "dependent rewrite" revealed by | herbelin |
| 2011-07-16 | This adds two option tables 'Printing Record' and 'Printing Constructor' | herbelin |
| 2011-07-16 | This is exactly the structure needed to handle controlling printing | herbelin |
| 2011-07-16 | This option disables the use of the '{| field := ... |}' notation | herbelin |
| 2011-07-16 | Some facts about functional extensionality (especially alternative | herbelin |
| 2011-07-16 | More lemmas relating the different equivalent formulations of eq_dep. | herbelin |
| 2011-07-16 | Tentative abbreviation "rew Heq in H" for eq_rect. (feedback welcome) | herbelin |
| 2011-07-16 | Changed name of internally defined "_sym" scheme to avoid confusion with Logi... | herbelin |
| 2011-07-16 | Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and... | herbelin |
| 2011-07-16 | Finally, pr_goal seems to work for printing v8.2 style goal in debugger. | herbelin |
| 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 |
