| Age | Commit message (Expand) | Author |
|---|
| 2017-01-26 | Adding a printer for Proof.proof reflecting the focusing layout. | Hugo Herbelin |
| 2016-11-05 | FIX: dev/include | Matej Kosik |
| 2016-08-17 | A fix to dev/include. | Hugo Herbelin |
| 2014-12-05 | More printers in tracer. | Hugo Herbelin |
| 2014-10-13 | Adding printers for ppproofview. | Hugo Herbelin |
| 2014-10-09 | Adding printer for named_context_val and Goal.goal in debugger. | Hugo Herbelin |
| 2014-10-07 | Adding a printer for hints. | Hugo Herbelin |
| 2014-08-26 | Debug RAKAM | Pierre Boutillier |
| 2014-06-11 | - Fix bug #3368, due to wrong use of the Cst_stack for projections. | Matthieu Sozeau |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | Fix issue #88: restrict_universe_context was wrongly forgetting about constra... | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-25 | print futures in caml toplevel too | Enrico Tassi |
| 2014-03-02 | Set officially the minimal OCaml requirement to 3.12.1 | Pierre Letouzey |
| 2013-10-29 | - install evar printer for debugging | msozeau |
| 2013-09-18 | At least made the evar type opaque! There are still 5 remaining unsafe | ppedrot |
| 2013-04-03 | Fix for bug #3017: wrong handling of the unresolvability status | msozeau |
| 2013-02-27 | remove a warning after Drop about print_hint_db | letouzey |
| 2012-08-05 | Revert "Fixing include printers" | pboutill |
| 2012-08-03 | Fixing include printers | ppedrot |
| 2011-12-18 | Suspending declaration of undefined debug printers. | herbelin |
| 2011-11-17 | Merge subinstances branch by me and Tom Prince. | msozeau |
| 2011-10-15 | debugging.txt: no more typing of #use "include" if using .ocamlinit | letouzey |
| 2011-08-04 | Fix unification: detect invalid evar instantiations due to scoping earlier. | msozeau |
| 2011-07-18 | Fixed a "feature" of "inversion" and "dependent rewrite" revealed by | herbelin |
| 2011-06-21 | Cleaning debugging printer relative to new proof engine. In | herbelin |
| 2011-02-07 | Factorize code of rewrite to make way for a new implementation using the | msozeau |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2009-11-13 | Remove useless ppevd (which is identical to ppevm) | glondu |
| 2009-10-25 | Improved the treatment of Local/Global options (noneffective Local on | herbelin |
| 2009-05-20 | - Fixing declarative mode in presence of high use of Change_evars nodes | herbelin |
| 2008-11-19 | Execute #rectypes directive in embedded OCaml toplevel... | glondu |
| 2008-03-18 | Hint for Debian users. | glondu |
| 2008-02-08 | Add printer for Pp.std_ppcmds... | msozeau |
| 2007-12-31 | Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,... | msozeau |
| 2007-12-07 | Ocaml toplevel convenience. | glondu |
| 2007-10-03 | Ajout de eelim, ecase, edestruct et einduction (expérimental). | herbelin |
| 2006-09-26 | mise a jour du nouveau ring et ajout du nouveau field, avant renommages | barras |
| 2006-01-11 | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin |
| 2005-12-26 | Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme... | herbelin |
| 2004-09-17 | restructuration des printers: proofs passe avant parsing | barras |
| 2004-09-08 | unification encore... | barras |
| 2003-04-16 | prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech... | letouzey |
| 2002-12-05 | Ajout affichage fconstr | herbelin |
| 2002-11-04 | ajout d'un printer pour les global_reference | letouzey |
| 2002-08-02 | Modules dans COQ\!\!\!\! | coq |
| 2002-02-15 | petits changements cosmetiques sur les tactiques | barras |
| 2001-11-06 | Suppression des local_constraints, des ctxtty et du focus. | clrenard |
| 2001-09-30 | Ajout du printer de tactiques + modif du Dynamic ocaml | delahaye |
| 2001-05-10 | ajout d'un afficher de contexte et d'une fonction constbody_of_string | letouzey |
