aboutsummaryrefslogtreecommitdiff
path: root/parsing/termast.mli
AgeCommit message (Expand)Author
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mécanis...herbelin
2005-01-03HUGE COMMITsacerdot
2004-07-16Nouvelle en-têteherbelin
2003-04-07Options d'affichage maintenant dans Constrexternherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-02-07petit nettoyage de kernel/inductivebarras
2001-11-05GROS COMMIT:barras
2001-05-29Facilites pour le debogguage des univers.coq
2001-03-15entetesfilliatr
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-24Nettoyageherbelin
2000-11-23Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;herbelin
2000-11-20Utilisation de global_reference dans rawconstrherbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...herbelin
2000-05-23Réparation bug d'affichage et affichage des instanciations par des {...}herbelin
2000-04-28Déplacement du type reference dans Termherbelin
2000-04-26Introduction d'un type constr_pattern pour les différents filtragesherbelin
2000-01-07Restructuration printer et parserherbelin
1999-12-13Poursuite intégration du Casesherbelin
1999-12-10Suppression Rel de rawconstr et correction de bugs d'affichageherbelin
1999-12-01Intégration du Termast et du Retyping de HH, et modifications connexesherbelin
1999-11-26module Extendfilliatr
1999-10-20 - documentation repertoire proofs/filliatr
1999-10-13organisation de trad (entre parsing/ et pretyping/)filliatr