index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
parsing
/
ppconstr.mli
Commit message (
Expand
)
Author
Age
*
Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...
herbelin
2006-05-30
*
Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsort
herbelin
2006-05-19
*
Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;
herbelin
2006-04-24
*
Déplacement de pr_arg et pr_opt de Ppconstr vers Util
herbelin
2006-01-21
*
Restructuration et simplification des fonctions d'affichage, de détypage
herbelin
2006-01-11
*
Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...
herbelin
2005-12-26
*
Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...
herbelin
2005-12-26
*
Compatibilité ocamlweb pour cible doc
herbelin
2005-01-21
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
Nouvelle en-tête
herbelin
2004-07-16
*
Globalisation des noms de tactiques dans les définitions de tactiques
herbelin
2003-04-07
*
*** empty log message ***
barras
2003-03-12
*
Problèmes et améliorations affichage; Changement Simpl
herbelin
2002-12-09
*
Passage à une représentation des fixpoints plus primitive dans constr_expr ...
herbelin
2002-11-15
*
Réforme de l'interprétation des termes :
herbelin
2002-11-14
*
Modules dans COQ\!\!\!\!
coq
2002-08-02
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29