| Commit message (Expand) | Author | Age |
|---|
| ... | |
| * | 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-04 |
| * | Some cleanup of Zcomplements | letouzey | 2011-07-01 |
| * | Cleanup of files related with power over Z. | letouzey | 2011-07-01 |
| * | 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-30 |
| * | update of Micromega doc |  fbesson | 2011-06-29 |
| * | 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-28 |
| * | 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-27 |
| * | 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-24 |
| * | cleanup of Zsgn | letouzey | 2011-06-23 |
| * | cleanup of Zmin and Zmax | letouzey | 2011-06-23 |
| * | Some more cleanup of Zorder | letouzey | 2011-06-23 |
| * | fix bug 2510: xml test is in the summary if it fails |  pboutill | 2011-06-22 |
| * | Follow-up concerning eqb / ltb / leb comparisons | letouzey | 2011-06-21 |
| * | Cleaning debugging printer relative to new proof engine. In |  herbelin | 2011-06-21 |
| * | 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 | 2011-06-20 |
| * | Some simplifications in NZDomain | letouzey | 2011-06-20 |
| * | Add compatibility option "-compat 8.3". | herbelin | 2011-06-20 |
| * | Fixing two typos introduced in r14217 and r14223 | herbelin | 2011-06-20 |
| * | Ensured that the transparency state is used when flag betaiota is on for apply. | herbelin | 2011-06-19 |
| * | Relaxed the constraint introduced in r14190 that froze the existing | herbelin | 2011-06-18 |
| * | Generalizing flag use_evars_pattern_unification into a flag | herbelin | 2011-06-18 |
| * | Activating flags betaiota by default for apply | herbelin | 2011-06-18 |
| * | r14204 and 14218 continued: completely removing test for bug #2490, | herbelin | 2011-06-18 |
| * | Partial backtrack on wrong r14204: bug #2490 still open. | herbelin | 2011-06-18 |
| * | The ad hoc version for first-order unification at toplevel of "?n args | herbelin | 2011-06-18 |
| * | Typo in CHANGES | herbelin | 2011-06-18 |
| * | add names of theorems in output |  jnarboux | 2011-06-18 |
| * | Customized accelerator maps for macos are globally installed (end to fix 2462) | pboutill | 2011-06-17 |
| * | Fix 2516: Utf8 font in Coqide Command panel | pboutill | 2011-06-17 |
| * | Fix bug 2269, program typechecker not used in Instance conclusions | msozeau | 2011-06-17 |
| * | refman nsatz |  pottier | 2011-06-16 |
| * | Tests de nsatz avec la geometrie | pottier | 2011-06-16 |
letouzey
msozeau
fbesson
pboutill
herbelin
jnarboux
pottier