aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* Fix compilation errorGravatar msozeau2011-06-30
* Keep obligation source information in ProgramGravatar msozeau2011-06-30
* Cleanup in SpecViaZGravatar letouzey2011-06-30
* Cleanup of NdigitsGravatar letouzey2011-06-30
* update of Micromega docGravatar fbesson2011-06-29
* Deletion of useless Zdigits_defGravatar letouzey2011-06-28
* Deletion of useless Zlog_defGravatar letouzey2011-06-28
* Deletion of useless Zsqrt_defGravatar letouzey2011-06-28
* Some cleanup of Zdiv and Zquot, deletion of useless Zdiv_defGravatar letouzey2011-06-28
* Some cleanup of Wf_Z.vGravatar letouzey2011-06-28
* improved tactic namesGravatar fbesson2011-06-28
* Some more cleanups (Zeven, auxiliary, Zbool, Zmisc, ZArith_base)Gravatar letouzey2011-06-27
* Znumtheory: a correct version of a compatibility Zdivide_introGravatar letouzey2011-06-27
* Clean-up of Znumtheory, deletion of Zgcd_defGravatar letouzey2011-06-24
* Numbers: a particular case of div_uniqueGravatar letouzey2011-06-24
* Numbers: change definition of divide (compat with Znumtheory)Gravatar letouzey2011-06-24
* cleanup of ZsgnGravatar letouzey2011-06-23
* cleanup of Zmin and ZmaxGravatar letouzey2011-06-23
* Some more cleanup of ZorderGravatar letouzey2011-06-23
* fix bug 2510: xml test is in the summary if it failsGravatar pboutill2011-06-22
* Follow-up concerning eqb / ltb / leb comparisonsGravatar letouzey2011-06-21
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Some migration of results from BinInt to NumbersGravatar letouzey2011-06-20
* Zcompare.destr_zcompare subsumed by case Z.compare_specGravatar letouzey2011-06-20
* Clean-up of Zcompare and ZorderGravatar letouzey2011-06-20
* Arithemtic: more concerning compare, eqb, leb, ltbGravatar letouzey2011-06-20
* Some simplifications in NZDomainGravatar letouzey2011-06-20
* Add compatibility option "-compat 8.3".Gravatar herbelin2011-06-20
* Fixing two typos introduced in r14217 and r14223Gravatar herbelin2011-06-20
* Ensured that the transparency state is used when flag betaiota is on for apply.Gravatar herbelin2011-06-19
* Relaxed the constraint introduced in r14190 that froze the existingGravatar herbelin2011-06-18
* Generalizing flag use_evars_pattern_unification into a flagGravatar herbelin2011-06-18
* Activating flags betaiota by default for applyGravatar herbelin2011-06-18
* r14204 and 14218 continued: completely removing test for bug #2490,Gravatar herbelin2011-06-18
* Partial backtrack on wrong r14204: bug #2490 still open.Gravatar herbelin2011-06-18
* The ad hoc version for first-order unification at toplevel of "?n argsGravatar herbelin2011-06-18
* Typo in CHANGESGravatar herbelin2011-06-18
* add names of theorems in outputGravatar jnarboux2011-06-18
* Customized accelerator maps for macos are globally installed (end to fix 2462)Gravatar pboutill2011-06-17
* Fix 2516: Utf8 font in Coqide Command panelGravatar pboutill2011-06-17
* Fix bug 2269, program typechecker not used in Instance conclusionsGravatar msozeau2011-06-17
* refman nsatzGravatar pottier2011-06-16
* Tests de nsatz avec la geometrieGravatar pottier2011-06-16
* git rebase -i mess consequenceGravatar pboutill2011-06-15
* Revert "Coqide now need lablgtk2.14.0" + Ide build system debuggingGravatar pboutill2011-06-14
* Making printing of backtick in Program reparsable (avoiding collision with "`(")Gravatar herbelin2011-06-14
* Regression files for bugs #2304 and #2490.Gravatar herbelin2011-06-14
* Fixing bug #2181 (Class mechanism can create dependencies over unnamedGravatar herbelin2011-06-14
* A few comments and a dev file to summarize issues with unificationGravatar herbelin2011-06-13
* Added full pattern-unification on Meta for tactic unification.Gravatar herbelin2011-06-13