aboutsummaryrefslogtreecommitdiff
path: root/parsing/printer.mli
AgeCommit message (Expand)Author
2012-05-29place all pretty-printing files in new dir printing/letouzey
2012-05-29global_reference migrated from Libnames to new Globnames, less deps in gramma...letouzey
2012-03-20Fixing alpha-conversion bug #2723 introduced in r12485-12486.herbelin
2011-11-23In emacs mode, prints a list of the dependent existential variables introducedaspiwack
2011-11-18Added a printing function to handle single evarsppedrot
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
2011-09-12Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...aspiwack
2011-06-10Revert "Check if recursive calls are guarded before printing "Proof completed"."pboutill
2011-05-26Check if recursive calls are guarded before printing "Proof completed".herbelin
2011-05-24Made the emacs-U option deprecated. Also removed the old codecourtieu
2011-05-21Restore display of notation when printing an inductive such as sigletouzey
2011-05-11Print Module (Type) M now tries to print more detailsletouzey
2011-03-07Reverted commit r13893 about propagation of more informativeherbelin
2011-03-07Added propagation of evars unification failure reasons for betterherbelin
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-22New script dev/tools/change-header to automatically update Coq files headers.herbelin
2010-06-06Added support for Ltac-matching terms with variables bound in the patternherbelin
2010-05-31deporting Coq specific code from ide to toplevel.vgross
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2010-04-29Move from ocamlweb to ocamdoc to generate mli documentationpboutill
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
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