aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2011-07-01Cleanup of files related with power over Z.letouzey
2011-06-30Fix compilation errormsozeau
2011-06-30Keep obligation source information in Programmsozeau
2011-06-30Cleanup in SpecViaZletouzey
2011-06-30Cleanup of Ndigitsletouzey
2011-06-29update of Micromega docfbesson
2011-06-28Deletion of useless Zdigits_defletouzey
2011-06-28Deletion of useless Zlog_defletouzey
2011-06-28Deletion of useless Zsqrt_defletouzey
2011-06-28Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defletouzey
2011-06-28Some cleanup of Wf_Z.vletouzey
2011-06-28improved tactic namesfbesson
2011-06-27Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)letouzey
2011-06-27Znumtheory: a correct version of a compatibility Zdivide_introletouzey
2011-06-24Clean-up of Znumtheory, deletion of Zgcd_defletouzey
2011-06-24Numbers: a particular case of div_uniqueletouzey
2011-06-24Numbers: change definition of divide (compat with Znumtheory)letouzey
2011-06-23cleanup of Zsgnletouzey
2011-06-23cleanup of Zmin and Zmaxletouzey
2011-06-23Some more cleanup of Zorderletouzey
2011-06-22fix bug 2510: xml test is in the summary if it failspboutill
2011-06-21Follow-up concerning eqb / ltb / leb comparisonsletouzey
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-06-20Some migration of results from BinInt to Numbersletouzey
2011-06-20Zcompare.destr_zcompare subsumed by case Z.compare_specletouzey
2011-06-20Clean-up of Zcompare and Zorderletouzey
2011-06-20Arithemtic: more concerning compare, eqb, leb, ltbletouzey
2011-06-20Some simplifications in NZDomainletouzey
2011-06-20Add compatibility option "-compat 8.3".herbelin
2011-06-20Fixing two typos introduced in r14217 and r14223herbelin
2011-06-19Ensured that the transparency state is used when flag betaiota is on for apply.herbelin
2011-06-18Relaxed the constraint introduced in r14190 that froze the existingherbelin
2011-06-18Generalizing flag use_evars_pattern_unification into a flagherbelin
2011-06-18Activating flags betaiota by default for applyherbelin
2011-06-18r14204 and 14218 continued: completely removing test for bug #2490,herbelin
2011-06-18Partial backtrack on wrong r14204: bug #2490 still open.herbelin
2011-06-18The ad hoc version for first-order unification at toplevel of "?n argsherbelin
2011-06-18Typo in CHANGESherbelin
2011-06-18add names of theorems in outputjnarboux
2011-06-17Customized accelerator maps for macos are globally installed (end to fix 2462)pboutill
2011-06-17Fix 2516: Utf8 font in Coqide Command panelpboutill
2011-06-17Fix bug 2269, program typechecker not used in Instance conclusionsmsozeau
2011-06-16refman nsatzpottier
2011-06-16Tests de nsatz avec la geometriepottier
2011-06-15git rebase -i mess consequencepboutill
2011-06-14Revert "Coqide now need lablgtk2.14.0" + Ide build system debuggingpboutill
2011-06-14Making printing of backtick in Program reparsable (avoiding collision with "`(")herbelin
2011-06-14Regression files for bugs #2304 and #2490.herbelin
2011-06-14Fixing bug #2181 (Class mechanism can create dependencies over unnamedherbelin
2011-06-13A few comments and a dev file to summarize issues with unificationherbelin