aboutsummaryrefslogtreecommitdiff
path: root/toplevel/vernacentries.ml
AgeCommit message (Expand)Author
2008-11-23Minor improvement to commit 11619herbelin
2008-11-23Fixed bug #2006 (type constraint on Record was not taken into account) +herbelin
2008-11-09More factorization of inductive/record and typeclasses: move classmsozeau
2008-11-05Move Record desugaring to constrintern and add ability to use notationsmsozeau
2008-11-05Nouvelle syntaxe pour écrire des records (co)inductifs :aspiwack
2008-10-11Backporting 11445 from 8.2 to trunk (negative conditions inherbelin
2008-10-03Minor fixes related to coqdoc and --interpolate and the dependentmsozeau
2008-09-14Add user syntax for creating hint databases [Create HintDb foomsozeau
2008-09-14In manual implicit arguments mode, do not enrich implicitsmsozeau
2008-08-04Évolutions diverses et variées.herbelin
2008-07-28Fixes in generalize_eqs/dependent induction to allow the user to specifymsozeau
2008-07-24Suite commit 11236notin
2008-07-22Correct implementation of discharging of implicit arguments and add newmsozeau
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-08Suite de la révision #11212notin
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-06-29Lissage de la gestion des chemins de chargement de fichiers :herbelin
2008-06-25Création du fichier dumpglob.ml, qui rassemble les fonctions de globalisatio...notin
2008-06-06Enhancements to coqdoc, better globalization of sections and modules.msozeau
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-22Strategy commands are now exportedbarras
2008-05-21refined the conversion oraclebarras
2008-05-12- Add -unicode flag to coqtop (sets Flags.unicode_syntax). Used tomsozeau
2008-05-10Correction bug #1842 + correction bug initialisation introduit dansherbelin
2008-05-08** Efficacité, bugs, robustesse CoqIDE **herbelin
2008-04-25Ajout de "Theorem id1 : t1 ... with idn : tn" pour partager la preuveherbelin
2008-04-15- Add "Global" modifier for instances inside sections with the usualmsozeau
2008-04-12Adding 'at' to rewrite, as it is already implemented in setoid_rewrite.msozeau
2008-04-05- Retour en arrière sur la capacité du nouvel apply à utiliser lesherbelin
2008-04-02Add the ability to specify the implicit status of section variables andmsozeau
2008-03-23Fix a bug found by B. Grégoire when declaring morphisms in modulemsozeau
2008-03-19Do another pass on the typeclasses code. Correct globalization of classmsozeau
2008-03-06Syntax changes in typeclasses, remove "?" for usual implicit argumentsmsozeau
2008-02-26Proper implicit arguments handling for assumptionsmsozeau
2008-02-22Merge with lmamane's private branch:lmamane
2008-02-01Beaoucoup de changements dans la representation interne des modules.soubiran
2008-01-18Change notation for setoid inequality, coerce objects before comparing them. ...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-17Print Assumptions est pret pour la release.aspiwack
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-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack