aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2011-06-07Catch AbstractionOverMeta as a unification failure in precatchable_exception.msozeau
2011-06-07Fix bug #2415: warn when closing modules or sections and some obligations are...msozeau
2011-06-07Fixed bug #2398: destruct ex2/sig2/sigT2 in Program, patch by Paolo Herms.msozeau
2011-06-07- Fix restrict_hyps to not allow filtering on a variable required to typechec...msozeau
2011-06-06Typo.gmelquio
2011-05-26Mini-test for etaherbelin
2011-05-26Partial fix for accepting bound variables with same name as implicitherbelin
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
2011-05-26Fixing discriminate for identity.herbelin
2011-05-25Q2R -> IQRfbesson
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-24Applying Enrico Tassi's patch for giving priority to delta over eta inherbelin
2011-05-23git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14152 85f007b7-540e-0...fbesson
2011-05-23ported r14149 from v8.3 branch: bug in checker (redefined global)barras
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
2011-05-20added support to handle division by a constant over Rfbesson
2011-05-19Remove useless "open Gc"glondu
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 06:54:39 +0000