aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel
Commit message (Expand)AuthorAge
* eviter redondance du message d'erreur (Error while reading / File)Gravatar barras2008-08-07
* Correction de bugs:Gravatar herbelin2008-08-05
* Report des commits 11297 et 11299 (nom Unnamed_theorem local caché parGravatar herbelin2008-08-04
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Fixes in generalize_eqs/dependent induction to allow the user to specifyGravatar msozeau2008-07-28
* - Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecGravatar herbelin2008-07-26
* Fixed bug #1904 (instances of evars were no longer substituted sinceGravatar herbelin2008-07-25
* Fix bug #1913, checking for unresolved evars which aren't obligations.Gravatar msozeau2008-07-24
* Suite commit 11236Gravatar notin2008-07-24
* Stop glob messages to be printed by default on stdout Gravatar letouzey2008-07-23
* 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