aboutsummaryrefslogtreecommitdiffhomepage
path: root/parsing/printer.ml
Commit message (Expand)AuthorAge
* Fixed some printing details for dependent evars in emacs mode. PatchGravatar courtieu2011-12-19
* Applied patches proposed suggested by Hendrik Tews to fix existentialGravatar courtieu2011-12-18
* In emacs mode, prints a list of the dependent existential variables introducedGravatar aspiwack2011-11-23
* Added a printing function to handle single evarsGravatar ppedrot2011-11-18
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
* Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the...Gravatar aspiwack2011-09-12
* Porting Hendrik's 8.3 patch for proof tree visualization under proofGravatar herbelin2011-08-30
* Revert "Check if recursive calls are guarded before printing "Proof completed"."Gravatar pboutill2011-06-10
* Check if recursive calls are guarded before printing "Proof completed".Gravatar herbelin2011-05-26
* Made the emacs-U option deprecated. Also removed the old codeGravatar courtieu2011-05-24
* Restore display of notation when printing an inductive such as sigGravatar letouzey2011-05-21
* Print Module (Type) M now tries to print more detailsGravatar letouzey2011-05-11
* Reverted commit r13893 about propagation of more informativeGravatar herbelin2011-03-07
* Added propagation of evars unification failure reasons for betterGravatar herbelin2011-03-07
* More {raw => glob} changes for consistencyGravatar glondu2010-12-24
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Remove some occurrences of "open Termops"Gravatar glondu2010-09-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Improved printing of Unfoldable constants in hints databases (usedGravatar herbelin2010-09-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Fixing spelling: pr_coma -> pr_commaGravatar herbelin2010-06-12
* Added support for Ltac-matching terms with variables bound in the patternGravatar herbelin2010-06-06
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* Integrate a few improvements on typeclasses and Program from the equations br...Gravatar msozeau2009-10-28
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Simplifying the call to print_no_goals and not calling it when no goalGravatar herbelin2009-06-11
* Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0Gravatar herbelin2009-06-06
* - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalenceGravatar herbelin2009-05-09
* Optionally list opaque constants in addition to axions/variables inGravatar msozeau2009-03-09
* - Added support for subterm matching in SearchAbout.Gravatar herbelin2008-12-29
* closed bug 1898: fold x in x; added a reordering primitive tacticGravatar barras2008-11-26
* - Fixed bug 1968 (inversion failing due to a Not_found bug introduced inGravatar herbelin2008-11-09
* duplicated open of PpconstrGravatar letouzey2008-10-21
* Évolutions diverses et variées.Gravatar herbelin2008-08-04
* Uniformisation du format des messages d'erreur (commencent par uneGravatar herbelin2008-07-17
* Various bug fixes in type classes and subtac:Gravatar msozeau2008-07-01
* Correction du problème de complexité de Print Assumptions :Gravatar aspiwack2008-05-27
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145)Gravatar herbelin2008-03-10
* Nettoyage de code en vue de la release. Plus de Warning: Unused Gravatar aspiwack2007-12-18
* Print Assumptions est pret pour la release.Gravatar aspiwack2007-12-17
* Plus de combinateurs sont passés de Util à Option. Le module Options Gravatar aspiwack2007-12-06
* Affichage de "thesis" seulement en mode déclaratifGravatar herbelin2007-07-18
* Factorisation des types dans l'affichage des paramètres des (Co)Inductif/RecordGravatar herbelin2007-06-30
* killing some more non-exhaustive patternsGravatar letouzey2007-06-26
* Corrections dans le Print Assumption. Les definitions locales ("Let") Gravatar aspiwack2007-05-30
* - Propagation des evars non résolues vers les with_bindings; permet par exempleGravatar herbelin2007-05-20
* Processor integers + Print assumption (see coqdev mailing list for the Gravatar aspiwack2007-05-11
* fin des conclusions multiplesGravatar corbinea2007-04-26
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 13:12:47 +0000