index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
interp
/
symbols.mli
Commit message (
Expand
)
Author
Age
*
Export compute_arguments_scope pour utilisation local a la construction des i...
herbelin
2004-03-27
*
Mise en place de motifs récursifs dans Notation; quelques simplifications au...
herbelin
2004-03-17
*
Localisation erreur interp_notation
herbelin
2004-02-12
*
Export information des references de notations pour coqdoc
herbelin
2004-01-21
*
Traitement plus clair, notamment pour Locate, de quand quoter les composantes...
herbelin
2003-11-22
*
Test de la reference principale plutot que le module dans lequel se trouve la...
herbelin
2003-11-12
*
Ajout notations pour motifs de Cases; renommage map_aconstr_with_binders_loc
herbelin
2003-11-01
*
Ajout de Print Visibility
herbelin
2003-10-28
*
Ajout 'Close Scope'.
herbelin
2003-09-30
*
Decouplage printing en v8 pour les interpretations de notations
herbelin
2003-09-26
*
Changement de la politique de V8only: V8only tout seul signifie
herbelin
2003-09-21
*
parsing
herbelin
2003-09-19
*
Activation déclaration automatique de scope d'arguments; affichage scopes d'...
herbelin
2003-09-12
*
Extension de Locate sur les symboles avec recherche de sous-chaînes; mise en...
herbelin
2003-06-10
*
Prise en compte des syntaxes v8 dans Uninterpreted Notation
herbelin
2003-04-29
*
Ajout "at next level" dans Notation
herbelin
2003-04-17
*
Ajout option "Local" à "Open Scope"
herbelin
2003-04-08
*
Prise en compte des scopes traversés dans les notations
herbelin
2002-12-15
*
Préparation à la prise en compte des changements de scopes internes aux not...
herbelin
2002-12-03
*
Réaffichage des Syntactic Definition (printer constr_expr).
herbelin
2002-11-26
*
Utilisation des niveaux de camlp4 pour gérer les niveaux de constr; amélior...
herbelin
2002-11-24
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14