aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-06-10Integrating onLastHypId into intro so that we can get the introductionherbelin
2011-06-10Call process_vernac_interp_error before calling Errors.print inherbelin
2011-06-10Coqide Menubar integration in MacOSpboutill
2011-06-10no more errors at _stubs.c.d generationpboutill
2011-06-10Menubar and toolbar in coqide using GtkUI & Gactions.pboutill
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
2011-06-10Fixes in pruning, do not fail if pruning is impossible due to typing constrai...msozeau
2011-06-10ring2, cring, nsatz avec type classe avec parametres plus notationspottier
2011-06-09More fixes in pruning/restriction of evars during unification.msozeau
2011-06-08Make Notation works with anonymous-level "Type".herbelin
2011-06-08Fixes in pruning in unification.msozeau
2011-06-07Fix bug #2399 in Program: used to build an ill-formed term due to a de Bruijn...msozeau
2011-06-07Fix bug #2335, fail if the search for reflexivity/symmetry/transitivity proof...msozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:07:51 +0000