aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/notation.ml
Commit message (Expand)AuthorAge
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Optimized need for delimiters when disjoint scopes for strings andGravatar herbelin2010-04-10
* Several bug-fixes and improvements of coqdocGravatar herbelin2010-03-29
* list, length, app are migrated from List to DatatypesGravatar letouzey2009-11-02
* Local/Global revision 12418 continuedGravatar herbelin2009-10-26
* New cleaning phase of the Local/Global option managementGravatar herbelin2009-10-26
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* This big commit addresses two problems:Gravatar soubiran2009-10-21
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Generalized the possibility to refer to a global name by a notationGravatar herbelin2009-09-11
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* - Cleaning phase of the interfaces of libnames.ml and nametab.mlGravatar herbelin2009-08-06
* Fix a small notation/scope bug:Gravatar vsiles2009-04-30
* pushed evar reduction in kernelGravatar barras2009-02-06
* Affichage des notations récursives:Gravatar herbelin2008-10-22
* Backporting 11445 from 8.2 to trunk (negative conditions inGravatar herbelin2008-10-11
* Correct implementation of discharging of implicit arguments and add newGravatar msozeau2008-07-22
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Documentation Prop<=Set et Arguments Scope GlobalGravatar herbelin2008-07-01
* Mises à jour test-suite + amélioration message d'erreur pour non-bug #1757Gravatar herbelin2008-05-07
* Add the ability to specify the implicit status of section variables andGravatar msozeau2008-04-02
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Factorisation des opérations sur le type option de Util dans un module Gravatar aspiwack2007-12-05
* Prise en compte réversibilité des notations de la forme "Notation Nil := @n...Gravatar herbelin2007-05-10
* Ajout de la possibilité de faire référence dans certains cas à un nomGravatar herbelin2007-04-28
* Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbo...Gravatar herbelin2007-02-24
* Suite commit restructuration discharge (application du type deGravatar herbelin2007-01-10
* Nouvelle approche pour le discharge modulaireGravatar herbelin2007-01-10
* Add a flush for a warning.Gravatar courtieu2006-10-23
* Annulation de l'essai de changement de sémantique du %scope (révision 9208).Gravatar herbelin2006-10-06
* Essai de changement de sémantique du %scope : Gravatar herbelin2006-10-05
* Correction bug #1179 (result of Notation.decompose_notation_key in wrong orderGravatar herbelin2006-09-23
* Standardisation nom option_app en option_mapGravatar herbelin2006-04-27
* Utilisation du section_path pour le parsing des notations primitives,Gravatar herbelin2006-02-04
* Adaptation message d'erreur au cas des stringGravatar herbelin2006-01-31
* Suppression de la dépendance en Map.fold de ocaml dont la sémantique aGravatar herbelin2006-01-24
* Automatisation de l'utilisation de token primitifs dans les motifs de filtrag...Gravatar herbelin2006-01-08
* Ajout d'un mécanisme d'interprétation et d'affichage pour les littéraux de...Gravatar herbelin2005-12-30
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Simplifification de vernac_expr li l'abandon du traducteurGravatar herbelin2005-12-23
* Nettoyage suite à la détection par défaut des variables inutilisées par o...Gravatar herbelin2005-11-08
* Moving centralised discharge into dispatched discharge_function; required to ...Gravatar herbelin2005-02-18
* HUGE COMMITGravatar sacerdot2005-01-03
* Renommage symbols.ml{,i} en notation.ml{,i} pour permettre le chargement de p...Gravatar herbelin2005-01-02