aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-12-04Fix priority of the Leibniz Setoid instance to 10 (thanks to M. Lassonmsozeau
2008-12-04Fixes for unification and substitution of metas under binders.msozeau
2008-12-03improved simplbarras
2008-12-02Add new directory for pre-compilation of files needed for further tests.herbelin
2008-12-02Miscellaneous fixes and improvements:herbelin
2008-12-02fixed kernel bug (de Bruijn) + test-suitebarras
2008-11-28another bug with simplbarras
2008-11-28Inductive parameters: nicer doc examples and error messageletouzey
2008-11-27Test case for previous commit.msozeau
2008-11-27Fix (?) a pattern matching compilation problem: msozeau
2008-11-27fixed non-exhaustive pattern matchingbarras
2008-11-27fixed bug 1791: simpl was performing eta expansionbarras
2008-11-27added tests for hyps reorderingbarras
2008-11-27fixing problem with CompCert: reordering resulting from tac change was not cl...barras
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
2008-11-26closed bug 1898: fold x in x; added a reordering primitive tacticbarras
2008-11-25correction bug 1997.soubiran
2008-11-24eventually fixing r11612barras
2008-11-24amelioration mineur du comportement de Functionjforest
2008-11-23first attempt to allow Function to deal with dependent pattern matching. This...jforest
2008-11-23- Synchronized subst_object with load_object (load_and_subst_objects)herbelin
2008-11-23Fine-tuning rewriting from "eq_true b": using <- to rewrite true to bherbelin
2008-11-23Minor improvement to commit 11619herbelin
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
2008-11-22Fixed bug in VernacExtend printing + missing vernacular printing rules +herbelin
2008-11-22- Fixed minor bug #1994 in the tactic chapter of the manual [doc]herbelin
2008-11-21fixed problem with r11612barras
2008-11-21fixed exponential behavior of evar unif (ground case)barras
2008-11-20correction of bug #2002jforest
2008-11-19Add implicit rules for native plugins (.cmxs)glondu
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
2008-11-19Fix typo in omega docglondu
2008-11-17integrate suggestions by B. Baydemir (see #1930)letouzey
2008-11-16Univ: two < instead of a Pervasives.compare on int (as suggested by X. Leroy)letouzey
2008-11-15Correct display of constraints for Print Universes "dumpfile"letouzey
2008-11-14Amélioration du README.doc et de l'installation de la docnotin
2008-11-14Restores behaviour of v8.1 for unification problems which fail (backport of 1...letouzey
2008-11-14Faster comparison of universesletouzey
2008-11-14make doc ne compilait plus la doc de stdlib (bug #1996)notin
2008-11-14Add missing test-suite files for closed bugs.msozeau
2008-11-14retour sur le commit 11579 qui faisait plante les contribs FSet et color.soubiran
2008-11-13Tentative d'amélioration de la robustesse des Makefile générés parnotin
2008-11-13git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11583 85f007b7-540e-0...barras
2008-11-12Correction du bug #1995notin
2008-11-12Les signatures des applications de foncteur sont précalculées, cela alourdi...soubiran
2008-11-10Makefile.build: an OPTFLAGS behind a bytecode ocamlc (which refuses -p)letouzey
2008-11-10Fix mixup between Record, Structure and Class by adding a new variant formsozeau
2008-11-10Fix bug reported by Mark Dickinson on Coq-Club about [setoid_rewrite] notmsozeau
2008-11-09- Correction erreur dans test output Notation.vherbelin
2008-11-09f_equal : solve an inefficiency issue (apply vs. simple apply)letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-24 10:40:32 +0000