aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Suite commit 11236Gravatar notin2008-07-21
* Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...Gravatar notin2008-07-18
* Affichage intempestif d'information de globalisation + numéro de version dan...Gravatar notin2008-07-18
* fixed indentation of subgoals for Show ScriptGravatar barras2008-07-17
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Autour du parsing:Gravatar herbelin2008-07-15
* Suite de la révision #11212Gravatar notin2008-07-08
* Fix implicit arguments in sections bug and check for resolution of evars whenGravatar msozeau2008-07-07
* Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...Gravatar notin2008-07-07
* - Improve [Context] vernacular to allow arbitrary binders, not justGravatar msozeau2008-07-07
* Fixes in handling of implicit arguments:Gravatar msozeau2008-07-04
* Lissage de la gestion des chemins de chargement de fichiers :Gravatar herbelin2008-06-29
* (Partial) fix for bug #1892, adding a missing newline.Gravatar msozeau2008-06-27
* Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...Gravatar notin2008-06-25
* Catch a Not_found exception in the Combined Scheme mechanism to hide an uglyGravatar vsiles2008-06-24
* Suppression de l'option -dump-glob et ajout d'une option -no-globGravatar notin2008-06-24
* Code cleanup in typeclasses, remove dead and duplicated code.Gravatar msozeau2008-06-21
* Fix bug #1889, correct globalization in class declarations.Gravatar msozeau2008-06-21
* - Implantation de la suggestion 1873 sur discriminate. Au final,Gravatar herbelin2008-06-21
* Fix bug in implementation of splitting of class constraints.Gravatar msozeau2008-06-18
* Fix bug in handling of classes and instances inside sections atGravatar msozeau2008-06-17
* Fixes w.r.t. let binders in class contexts and Add ParametricGravatar msozeau2008-06-17
* Better typeclass error messages, always giving the full set ofGravatar msozeau2008-06-17
* Correction bug 1878 (utilisation de extend_evar déplacée là où uneGravatar herbelin2008-06-14
* Temporary fix for bug #1876, printing fails because of unresolvedGravatar msozeau2008-06-13
* Optionally (and by default) split typeclasses evars into connected Gravatar msozeau2008-06-11
* - Officialisation de la notation "pattern c at -1" (cf wish 1798 sur coq-bugs)Gravatar herbelin2008-06-10
* - Correction bug 1841 (identificateurs incorrects avec Subclass)Gravatar herbelin2008-06-10
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* Enhancements to coqdoc, better globalization of sections and modules.Gravatar msozeau2008-06-06
* 2-3 petites modifs pour la compilation sous Windows...Gravatar notin2008-06-06
* Fixes incorrect handling of existing existentials variables inGravatar msozeau2008-06-03
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
* Improvements on coqdoc by adding more information into .globGravatar msozeau2008-05-30
* - Nouvelle option "Set Printing Existential Instances" pour forcerGravatar herbelin2008-05-25
* - Fix bug #1858, Hint Unfold calling the wrong locate function.Gravatar msozeau2008-05-23
* Strategy commands are now exportedGravatar barras2008-05-22
* refined the conversion oracleGravatar barras2008-05-21
* Fix globalization bug in class_tactics and refactorize instanceGravatar msozeau2008-05-19
* - Fix bug related to indices of fixpoints.Gravatar msozeau2008-05-13
* - Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used toGravatar msozeau2008-05-12
* - Cleanup parsing of binders, reducing to a single production for allGravatar msozeau2008-05-11
* Correction bug #1842 + correction bug initialisation introduit dansGravatar herbelin2008-05-10
* - Prise en compte de l'unicode dans la fonction hdchar (elle fournissait desGravatar herbelin2008-05-10
* ** Efficacité, bugs, robustesse CoqIDE **Gravatar herbelin2008-05-08
* Integration of theories/Ints into theories/Numbers, part 3: fixing forgotten ...Gravatar letouzey2008-05-07
* Postpone the search for the recursive argument index from the user givenGravatar msozeau2008-05-06
* Mise en place d'un algorithme d'inversion des contraintes de type lorsGravatar herbelin2008-05-05
* More emacs-friendly error messages.Gravatar glondu2008-05-05