aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-06-13Added full pattern-unification on Meta for tactic unification.herbelin
2011-06-13Added a flag to restrict conversion in tactic unification on theherbelin
2011-06-13Another bug of Scheme Induction (generated names dep/nodep were swapped).herbelin
2011-06-13Fixing an anomaly in Scheme Induction.herbelin
2011-06-12Oups, typo in previous commitherbelin
2011-06-12Removed what looks like a (very old) useless f.o. unification passherbelin
2011-06-12Added a new flag for freezing evars in tactic unification. Used thisherbelin
2011-06-12Rather quick hack to avoid using notations involving "Type" whenherbelin
2011-06-11Coqide now need lablgtk2.14.0pboutill
2011-06-10Updated CHANGES (info, Show Script, rephrasing).herbelin
2011-06-10Moved allow_K to a unification flagherbelin
2011-06-10Fixing another bug with "_" intro pattern.herbelin
2011-06-10Fixing the "buggy" first_name and prepare multi-induction.herbelin
2011-06-10Made use of "_" in repeated use of intros_patterns work (withherbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 14:09:04 +0000