aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/ppconstr.mli
Commit message (Expand)AuthorAge
* Merge from Lionel Elie Mamane's private branch:Gravatar lmamane2007-01-10
* Généralisation de with_occurrence (ex occurrence) et de red_expr pour perme...Gravatar herbelin2006-05-30
* Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortGravatar herbelin2006-05-19
* Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;Gravatar herbelin2006-04-24
* Déplacement de pr_arg et pr_opt de Ppconstr vers UtilGravatar herbelin2006-01-21
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Renommage des Pp*new en Pp* (et déplacement dans parsing); renommage des G_*...Gravatar herbelin2005-12-26
* Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...Gravatar herbelin2005-12-26
* Compatibilité ocamlweb pour cible docGravatar herbelin2005-01-21
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* Nouvelle en-têteGravatar herbelin2004-07-16
* Globalisation des noms de tactiques dans les définitions de tactiquesGravatar herbelin2003-04-07
* *** empty log message ***Gravatar barras2003-03-12
* Problèmes et améliorations affichage; Changement SimplGravatar herbelin2002-12-09
* Passage à une représentation des fixpoints plus primitive dans constr_expr ...Gravatar herbelin2002-11-15
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...Gravatar herbelin2002-05-29