aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2008-07-26- Pour CoRN, rétablissement notations Qgt/Qge (mais cette fois avecherbelin
2008-07-25Fixed bug #1904 (instances of evars were no longer substituted sinceherbelin
2008-07-24Fix bug #1913, checking for unresolved evars which aren't obligations.msozeau
2008-07-24Suite commit 11236notin
2008-07-23Stop glob messages to be printed by default on stdout letouzey
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
2008-07-21Suite commit 11236notin
2008-07-18Rétablissement de l'option -dump-glob de coq top et de l'option -glob-from d...notin
2008-07-18Affichage intempestif d'information de globalisation + numéro de version dan...notin
2008-07-17fixed indentation of subgoals for Show Scriptbarras
2008-07-17Uniformisation du format des messages d'erreur (commencent par uneherbelin
2008-07-15Autour du parsing:herbelin
2008-07-08Suite de la révision #11212notin
2008-07-07Fix implicit arguments in sections bug and check for resolution of evars whenmsozeau
2008-07-07Utilisation de try_locate_qualified_library au lieu de locate_qualified_libra...notin
2008-07-07- Improve [Context] vernacular to allow arbitrary binders, not justmsozeau
2008-07-04Fixes in handling of implicit arguments:msozeau
2008-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-06-27(Partial) fix for bug #1892, adding a missing newline.msozeau
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