aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-24Catch a Not_found exception in the Combined Scheme mechanism to hide an uglyvsiles
2008-06-24Suppression de l'option -dump-glob et ajout d'une option -no-globnotin
2008-06-21Code cleanup in typeclasses, remove dead and duplicated code.msozeau
2008-06-21Fix bug #1889, correct globalization in class declarations.msozeau
2008-06-21- Implantation de la suggestion 1873 sur discriminate. Au final,herbelin
2008-06-18Fix bug in implementation of splitting of class constraints.msozeau
2008-06-17Fix bug in handling of classes and instances inside sections atmsozeau
2008-06-17Fixes w.r.t. let binders in class contexts and Add Parametricmsozeau
2008-06-17Better typeclass error messages, always giving the full set ofmsozeau
2008-06-14Correction bug 1878 (utilisation de extend_evar déplacée là où uneherbelin
2008-06-13Temporary fix for bug #1876, printing fails because of unresolvedmsozeau
2008-06-11Optionally (and by default) split typeclasses evars into connected msozeau
2008-06-10- Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)herbelin
2008-06-10- Correction bug 1841 (identificateurs incorrects avec Subclass)herbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
2008-06-062-3 petites modifs pour la compilation sous Windows...notin
2008-06-03Fixes incorrect handling of existing existentials variables inmsozeau
2008-06-03Fix setoid_rewrite documentation examples.msozeau
2008-05-30Improvements on coqdoc by adding more information into .globmsozeau
2008-05-25- Nouvelle option "Set Printing Existential Instances" pour forcerherbelin
2008-05-23- Fix bug #1858, Hint Unfold calling the wrong locate function.msozeau
2008-05-22Strategy commands are now exportedbarras
2008-05-21refined the conversion oraclebarras
2008-05-19Fix globalization bug in class_tactics and refactorize instancemsozeau
2008-05-13- Fix bug related to indices of fixpoints.msozeau
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-11- Cleanup parsing of binders, reducing to a single production for allmsozeau
2008-05-10Correction bug #1842 + correction bug initialisation introduit dansherbelin
2008-05-10- Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desherbelin
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
2008-05-07Integration of theories/Ints into theories/Numbers, part 3: fixing forgotten ...letouzey
2008-05-06Postpone the search for the recursive argument index from the user givenmsozeau
2008-05-05Mise en place d'un algorithme d'inversion des contraintes de type lorsherbelin
2008-05-05More emacs-friendly error messages.glondu
2008-04-28Petites corrections vis à vis des commits 10860, 10859, 10850herbelin
2008-04-27Quelques bricoles autour de l'unification:herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-24Fix bug #1844, generalize implementation to handle and combination ofmsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-23Added frozen state after each command.courtieu
2008-04-17Bug squashing day !msozeau
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2008-04-12Add the ability to specify what to do with free variables in instancemsozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-11Check that no evars remain in instance types earlier at Instancemsozeau
2008-04-08- A little cleanup in Classes/*. Separate standard morphisms onmsozeau
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin