aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/symbols.ml
Commit message (Expand)AuthorAge
* Correction du bug 335 et Export/Require Export dans un moduleGravatar coq2003-10-07
* cosmetiqueGravatar herbelin2003-10-01
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
* Decouplage printing en v8 pour les interpretations de notationsGravatar herbelin2003-09-26
* parsingGravatar herbelin2003-09-19
* Activation déclaration automatique de scope d'argumentsGravatar herbelin2003-09-12
* Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...Gravatar herbelin2003-06-10
* Prise en compte des syntaxes v8 dans Uninterpreted NotationGravatar herbelin2003-04-29
* Ajout "at next level" dans NotationGravatar herbelin2003-04-17
* Ajout option 'Local' à Infix et NotationGravatar herbelin2003-04-11
* Application de l'absence d'export aux modulesGravatar herbelin2003-04-08
* Ajout option "Local" à "Open Scope"Gravatar herbelin2003-04-08
* Prise en compte des scopes traversés dans les notationsGravatar herbelin2002-12-15
* Préparation à la prise en compte des changements de scopes internes aux not...Gravatar herbelin2002-12-03
* Bug exceptionGravatar herbelin2002-11-28
* Réaffichage des Syntactic Definition (printer constr_expr).Gravatar herbelin2002-11-26
* Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...Gravatar herbelin2002-11-24
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14