aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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
2008-11-09better fix for #1931 by using sort_ofletouzey
2008-11-09Oops... forgot to commit a file related to r11561.msozeau
2008-11-09Add test-suite file related to discussion of syntax of implicit binders.msozeau
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-09- Fixed bug 1968 (inversion failing due to a Not_found bug introduced inherbelin
2008-11-08Apply vmconv if there are no _undefined_ evars around.msozeau
2008-11-07Slight change of the semantics of user-given casts: they don't reallymsozeau
2008-11-07- Ajout possibilité de lancer ocamldebug sur coqideherbelin
2008-11-07Suite #11533notin
2008-11-07Correction du bug #1926notin
2008-11-07Add some example uses of the new record features in Record.v:msozeau
2008-11-07Fix a bug in the specialization by unification tactic related to the problemsmsozeau
2008-11-07Add the ability to give a specific tactic to solve each obligation inmsozeau
2008-11-07Fix universe problem appearing ConCaT using the existing infrastructure formsozeau
2008-11-06Cosmetic: no more whitespace at end of lines in extraction filesletouzey
2008-11-06Correction d'un petit bug en cas de redéfintion par l'utilisateur de variabl...notin
2008-11-05Minor fixes:msozeau
2008-11-05Port [rewrite] tactics to open terms. Currently no check that evarsmsozeau
2008-11-05Fix in the unification algorithm using evars: unify types of evarmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-11-05Suite commit 11539 sur notation Record dans (Co)Inductive (MAJherbelin
2008-11-05Petit bug dans le commit précédent.aspiwack
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-11-05Better extraction renaming phase (fix #1914 plus other non-reported bugs)letouzey
2008-11-04Adaptation to ocaml 3.11 new semantics of String.index_from (see bug #1974)herbelin
2008-11-042 petites améliorations de coq_makefile (traitement des .ml4 + cibles géné...notin
2008-11-02Fix CAMLHLIB (due to r11358) (Closes: #1986)glondu
2008-11-02test-suite/ideal-features/{apply.v -> eapply_evar.v}glondu
2008-10-31Ajout d'une option -raw pour Coqdoc (sortie en texte brut)notin
2008-10-31allowed patternidents starting with an '_'amahboub
2008-10-30The lexer is changer to break former PATTERNIDENT into two tokens.amahboub
generated by cgit v1.2.3 (git 2.25.1) at 2026-07-19 12:37:42 +0000