aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/symbols.mli
Commit message (Expand)AuthorAge
* Localisation erreur interp_notationGravatar herbelin2004-02-12
* Export information des references de notations pour coqdocGravatar herbelin2004-01-21
* Traitement plus clair, notamment pour Locate, de quand quoter les composantes...Gravatar herbelin2003-11-22
* Test de la reference principale plutot que le module dans lequel se trouve la...Gravatar herbelin2003-11-12
* Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_locGravatar herbelin2003-11-01
* Ajout de Print VisibilityGravatar herbelin2003-10-28
* Ajout 'Close Scope'.Gravatar herbelin2003-09-30
* Decouplage printing en v8 pour les interpretations de notationsGravatar herbelin2003-09-26
* Changement de la politique de V8only: V8only tout seul signifieGravatar herbelin2003-09-21
* parsingGravatar herbelin2003-09-19
* Activation déclaration automatique de scope d'arguments; affichage scopes d'...Gravatar 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" à "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
* 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