| Age | Commit message (Expand) | Author |
|---|
| 2012-05-29 | place all pretty-printing files in new dir printing/ | letouzey |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey |
| 2012-03-30 | Typo in a message. | aspiwack |
| 2012-03-20 | Fixing alpha-conversion bug #2723 introduced in r12485-12486. | herbelin |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-02-07 | A "Grab Existential Variables" to transform the unresolved evars at the end o... | aspiwack |
| 2011-12-19 | Fixed some printing details for dependent evars in emacs mode. Patch | courtieu |
| 2011-12-18 | Applied patches proposed suggested by Hendrik Tews to fix existential | courtieu |
| 2011-11-23 | In emacs mode, prints a list of the dependent existential variables introduced | aspiwack |
| 2011-11-18 | Added a printing function to handle single evars | ppedrot |
| 2011-10-25 | First attempt at making Print Assumption compatible with opaque modules (fix ... | letouzey |
| 2011-09-12 | Adds a new command Show Goal (e.g. Show Goal "42") printing a goal using the... | aspiwack |
| 2011-08-30 | Porting Hendrik's 8.3 patch for proof tree visualization under proof | herbelin |
| 2011-06-10 | Revert "Check if recursive calls are guarded before printing "Proof completed"." | pboutill |
| 2011-05-26 | Check if recursive calls are guarded before printing "Proof completed". | herbelin |
| 2011-05-24 | Made the emacs-U option deprecated. Also removed the old code | courtieu |
| 2011-05-21 | Restore display of notation when printing an inductive such as sig | letouzey |
| 2011-05-11 | Print Module (Type) M now tries to print more details | letouzey |
| 2011-03-07 | Reverted commit r13893 about propagation of more informative | herbelin |
| 2011-03-07 | Added propagation of evars unification failure reasons for better | herbelin |
| 2010-12-24 | More {raw => glob} changes for consistency | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-09-28 | Remove some occurrences of "open Termops" | glondu |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-02 | Improved printing of Unfoldable constants in hints databases (used | herbelin |
| 2010-07-24 | Updated all headers for 8.3 and trunk | herbelin |
| 2010-06-12 | Fixing spelling: pr_coma -> pr_comma | herbelin |
| 2010-06-06 | Added support for Ltac-matching terms with variables bound in the pattern | herbelin |
| 2010-04-29 | Remove the svn-specific $Id$ annotations | letouzey |
| 2010-04-22 | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack |
| 2009-10-28 | Integrate a few improvements on typeclasses and Program from the equations br... | msozeau |
| 2009-09-17 | Delete trailing whitespaces in all *.{v,ml*} files | glondu |
| 2009-06-11 | Simplifying the call to print_no_goals and not calling it when no goal | herbelin |
| 2009-06-06 | Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0 | herbelin |
| 2009-05-09 | - Adding "Hint Resolve ->" and "Hint Resolve <-" for declaration of equivalence | herbelin |
| 2009-03-09 | Optionally list opaque constants in addition to axions/variables in | msozeau |
| 2008-12-29 | - Added support for subterm matching in SearchAbout. | herbelin |
| 2008-11-26 | closed bug 1898: fold x in x; added a reordering primitive tactic | barras |
| 2008-11-09 | - Fixed bug 1968 (inversion failing due to a Not_found bug introduced in | herbelin |
| 2008-10-21 | duplicated open of Ppconstr | letouzey |
| 2008-08-04 | Évolutions diverses et variées. | herbelin |
| 2008-07-17 | Uniformisation du format des messages d'erreur (commencent par une | herbelin |
| 2008-07-01 | Various bug fixes in type classes and subtac: | msozeau |
| 2008-05-27 | Correction du problème de complexité de Print Assumptions : | aspiwack |
| 2008-04-24 | - Add pretty-printers for Idpred, Cpred and transparent_state, used for | msozeau |
| 2008-03-10 | Une passe sur l'unification des evars (suite aux commits 10124, 10125, 10145) | herbelin |
| 2007-12-18 | Nettoyage de code en vue de la release. Plus de Warning: Unused | aspiwack |
| 2007-12-17 | Print Assumptions est pret pour la release. | aspiwack |
