aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2008-01-30Support for substructures in classes using :> notationmsozeau
2008-01-30Add occurence extra argmsozeau
2008-01-30Debug 0-ary typeclasses support, use new redefinition support for default tacticmsozeau
2008-01-30Add list_iter3 msozeau
2008-01-30Add some keywordmsozeau
2008-01-29Added full documentation for mathematical mode (draft version)corbinea
2008-01-29Correction du bug #1785notin
2008-01-24Nicer proofs.roconnor
2008-01-24remove Fourier Failure warnings.roconnor
2008-01-24Prove the decidability of arithmetical statements using the real numbers.roconnor
2008-01-24Fermeture du bug #1754notin
2008-01-24Keep the Z_scope local to this file.roconnor
2008-01-23Changing R to a local definition so that it isn't exported.roconnor
2008-01-23Ajout d'un test pour le bug #1779notin
2008-01-23Ajout d'un test pour le mode déclaratif + test pour le bug #1776notin
2008-01-23Typonotin
2008-01-22Ajout de sauts de ligne dans l'affichage des scripts (cf commit 10445)notin
2008-01-22Adding Zdiv_le_compat_lthery
2008-01-22Récupération d'une exception Not_foundnotin
2008-01-21Correction du bug #1754notin
2008-01-20cosmetics: after an extract inductive to bool, let's use if then elseletouzey
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-18bug in accessing n-th abstractionbarras
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2008-01-17Fix Makefile bug, using .v instead of .vo and document SetoidDec.vmsozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-17fixed script printingcorbinea
2008-01-17Bug in sqrt321thery
2008-01-15Fix backtracking bugs:lmamane
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-11Amélioration de la génération des graphes de dépendancesnotin
2008-01-11implements a better way to respect the Unix convention that processes receive...bertot
2008-01-11Amélioration de la génération des graphes de dépendances (utilisation de ...notin
2008-01-10Correction du bug #1770: il semble que la recherche insensible à la casse ne...notin
2008-01-09Correction of bug #1769jforest
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2008-01-07Ajout d'une explication dans la FAQ pour le bug avec MOD4 sous Coqidenotin
2008-01-07Remove spurious .d, better tactics.msozeau
2008-01-07Completion of 10427...herbelin
2008-01-05Fix a naming bug reported by Arnaud Spiwack, allow instance search to create ...msozeau
2008-01-05Correction bug #1749 (datant de l'implantation des or-patterns) +herbelin
2008-01-05Fixed bug 1761 (unexpected anomaly when constructor type has invalidherbelin
2008-01-05Added a note about the ambiguity of the syntax "qualid" in "tacarg"herbelin
2008-01-05Standardisation du format des références croisées vers Figure, Section, Ch...herbelin
2008-01-04more user-friendly versions of some properties lemmas in FSets/FMapletouzey
2008-01-04Add partial setoids in theories/Classes, add SetoidDec class for setoids with...msozeau
2008-01-04Prise en compte de CAMLP4LIB via fichier configure plutôt que dynamiquementherbelin
2008-01-02Implicit arguments in class field declarationsmsozeau
2008-01-02Better resolution of implicit parameters in typeclass binders, add extensiona...msozeau
2007-12-31Fix name capture bug and call the right pretyper in subtac.msozeau