aboutsummaryrefslogtreecommitdiff
path: root/parsing/printer.mli
AgeCommit message (Expand)Author
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2008-08-04Évolutions diverses et variées.herbelin
2008-07-01Various bug fixes in type classes and subtac:msozeau
2008-05-27Correction du problème de complexité de Print Assumptions :aspiwack
2008-04-24- Add pretty-printers for Idpred, Cpred and transparent_state, used formsozeau
2007-12-17Print Assumptions est pret pour la release.aspiwack
2007-05-20- Propagation des evars non résolues vers les with_bindings; permet par exempleherbelin
2007-05-11Processor integers + Print assumption (see coqdev mailing list for the aspiwack
2007-01-10Merge from Lionel Elie Mamane's private branch:lmamane
2006-11-17The emacs-U option now does not output *any* char above 250.courtieu
2006-10-19coqide: affichage des sous-buts et hypothèses et métas comme types deherbelin
2006-09-20Declarative Proof Language: main commitcorbinea
2006-05-19Ajout de pr_sort, extern_sort, detype_sort et renommage pr_sort en pr_rawsortherbelin
2006-04-24Export de pr_lconstr_pattern, pr_lconstr_pattern_env et pr_lpattern_expr;herbelin
2006-01-12Compatibilité prtermherbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-07-15Add some debug printing functions.coq
2005-01-21Compatibilité ocamlweb pour cible docherbelin
2004-12-07* added subst_evaluable_referencesacerdot
2004-12-07The type Pattern.constr_label was isomorphic to Libnames.global_reference.sacerdot
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-07-16Nouvelle en-têteherbelin
2003-03-12*** empty log message ***barras
2002-08-02Modules dans COQ\!\!\!\!coq
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-02-07petit nettoyage de kernel/inductivebarras
2001-11-05GROS COMMIT:barras
2001-03-15entetesfilliatr
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
2000-11-23Affichage des paths avec des '.'; print_id, print_sp -> pr_id, pr_sp;herbelin
2000-11-20Ajout pr_global_reference et is_visibleherbelin
2000-10-18Simplifications autour de typed_type (renommé types par analogie avec sorts)...herbelin
2000-10-18Renommage canonique :herbelin
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
2000-06-01Mise en place d'un choix constr/typed_type en remplacement de certains Castherbelin
2000-05-26Modification messages d'erreurs, possibilité de n'importe quel constr dans l...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-31Export gentermpr avec renommageherbelin
2000-01-07Restructuration printer et parserherbelin
1999-12-15Nouveaux types 'constructor' et 'inductive' dans Term;herbelin
1999-12-09Ajout des messages d'erreurs de Casesherbelin
1999-12-03modules profile, Coqinit et Coqtop (=main)filliatr
1999-12-01Ajout des fonctions prpattern et prrawtermherbelin
1999-12-01printersfilliatr
1999-11-26module Pretty (partiellement)filliatr
1999-11-26module Extendfilliatr
1999-10-13organisation de trad (entre parsing/ et pretyping/)filliatr