aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2008-01-30Support for substructures in classes using :> notationmsozeau
2008-01-30Debug 0-ary typeclasses support, use new redefinition support for default tacticmsozeau
2008-01-18Fix bug #1778, better typeclass error messages. Move Obligations Tactic to a ...msozeau
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2008-01-17Add new LetPattern construct to replace dest. syntax: let| pat := t in b is b...msozeau
2008-01-15Generalize instance declarations to any context, better name handling. Add ho...msozeau
2008-01-07Cleaner quantifiers for type classes, breaks clrewrite for the moment but imp...msozeau
2008-01-05Fixed bug 1761 (unexpected anomaly when constructor type has invalidherbelin
2008-01-02Implicit arguments in class field declarationsmsozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-18Nettoyage de code en vue de la release. Plus de Warning: Unused aspiwack
2007-12-17Print Assumptions est pret pour la release.aspiwack
2007-12-13migration of ide/utf8.v to theories/Unicode/Utf8.vletouzey
2007-12-06Plus de combinateurs sont passés de Util à Option. Le module Options aspiwack
2007-12-05Factorisation des opérations sur le type option de Util dans un module aspiwack
2007-11-09Nettoyage de Print Assumptions :aspiwack
2007-11-08Prise en compte des notations "alias" dans la globalisation des coercions.herbelin
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
2007-09-30Ajout infos de débogage de "universe inconsistency" quand option Setherbelin
2007-09-28On Linux, we read /proc/self/exe to get the executable's path insteadglondu
2007-09-28Modification of the Scheme command.vsiles
2007-09-15* Adding compability with ocaml 3.10 + camlp5 (rework of letouzey
2007-09-06Uniformisation politique de nommage evd/isevars (evd si evar_defs,herbelin
2007-08-30Mise à jour des paramètres Whelp et ajouts d'options Set Whelp Serverherbelin
2007-08-24Report 10087, 10089, 10090 de 8.1 vers trunk (compatibilité camlp5 et -recty...herbelin
2007-08-24Utilisation plus précise de la contrainte de type pour interpréter lesherbelin
2007-08-20Modification de l'initialisation des chemins de la librairie standardnotin
2007-07-13New bootstrapping, improved, Makefile systemcorbinea
2007-07-07If a fixpoint is not written with an explicit { struct ... }, then letouzey
2007-06-30- Ajout de la possibilité d'utiliser la notation Record pour lesherbelin
2007-05-29Correction d'un bug dans l'affichage du message d'erreur real_cleanherbelin
2007-05-28Contrôle de la compatibilité de apply via une information dans lesherbelin
2007-05-25Modification of VernacScheme to handle a new scheme: Equality (equality invsiles
2007-05-17Nettoyage et standardisation des messages d'erreurs.herbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-05-06Nouveaux changements autour des implicites (notamment suite àherbelin
2007-04-29Multiples changements autour des implicites :herbelin
2007-04-29Correction bug #1507 (report révision 9807 de v8.1 vers trunk)herbelin
2007-04-25New keyword "Inline" for Parameters and Axioms for automatic soubiran
2007-04-17Reorder hook and printing of message, more natural this way.msozeau
2007-04-17 Added the option to set/unset the automatic generation of elimination schemesvsiles
2007-03-28Support for implicit formal argument types in Program ; parse types in type s...msozeau
2007-03-19Add a parameter to QuestionMark evar kind to say it can be turned into an obl...msozeau
2007-03-15Suppression argument pattern_source du case_info (code jamais utilisé)herbelin
2007-03-15Prévention notations récursives sans terminal à gauche et qui font bouclerherbelin
2007-03-09bug#1434 importing fonctor arguments, now it works.soubiran
2007-02-24Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...herbelin
2007-02-24Achèvement commit 9677 (suppression résidu v7 dans PrintGrammar)herbelin
2007-02-24Suppression d'un résidu de la syntaxe v7 (Print Grammar avec univ)herbelin
2007-02-21Utilisation de l'environnement pour l'affichage de certains messages d'erreursherbelin