| Commit message (Expand) | Author | Age |
|---|
| * | More open in base_include |  Hugo Herbelin | 2014-06-28 |
| * | - Fix in kernel conversion not folding the universe constraints |  Matthieu Sozeau | 2014-05-26 |
| * | Remove Lemmas from base_include, it's not linked in dev/printers anymore | Matthieu Sozeau | 2014-05-06 |
| * | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
| * | Updated debugging printers | Hugo Herbelin | 2014-04-01 |
| * | app_node, stack, state printers |  Pierre Boutillier | 2014-02-24 |
| * | 'Pretty' printer for wf_paths | Pierre | 2014-01-11 |
| * | Fix base_include: Toplevel-->Coqloop, Constrintern.intern_constr without evd |  Pierre Letouzey | 2014-01-08 |
| * | Remove the Hiddentac module. |  Arnaud Spiwack | 2013-11-25 |
| * | Removes Refine from the dev tools now that the module has been deleted. |  aspiwack | 2013-11-02 |
| * | Robust display of NotConvertibleTypeField errors (fix #3008, #2995) |  letouzey | 2013-03-21 |
| * | Update debug code according to reorganization into modules. |  msozeau | 2013-02-27 |
| * | Adapt dev/base_include to new Declarations | letouzey | 2013-02-27 |
| * | Added Evarsolve to the list of modules to open for debugging. |  herbelin | 2013-02-21 |
| * | Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterp | letouzey | 2012-10-16 |
| * | 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 |
| * | Strongly reduce the dependencies of grammar.cma, modulo two hacks | letouzey | 2012-05-29 |
| * | lib directory is cut in 2 cma. |  pboutill | 2012-04-12 |
| * | Removing Dhyp from debugger. | herbelin | 2012-04-06 |
| * | Everything compiles again. | msozeau | 2012-03-14 |
| * | Debugger vs tracer: Two different behaviors wrt printing: The debugger | herbelin | 2012-02-01 |
| * | dev/base_include: display a nice message at the end of the load | letouzey | 2011-10-15 |
| * | dev/base_include: no more mod_self_id | letouzey | 2011-04-26 |
| * | - Remove create_evar_defs | msozeau | 2011-04-13 |
| * | Fix dev/base_include after change of constant_body | letouzey | 2011-04-06 |
| * | Rename rawterm.ml into glob_term.ml |  glondu | 2010-12-23 |
| * | Change of nomenclature: rawconstr -> glob_constr | glondu | 2010-12-23 |
| * | Quick fix for having clenv debug printer working in trunk. | herbelin | 2010-06-18 |
| * | Here comes the commit, announced long ago, of the new tactic engine. | aspiwack | 2010-04-22 |
| * | A bit of cleaning around name generation + creation of dedicated file namegen.ml | herbelin | 2009-11-09 |
| * | Fixed "Scheme Equality" when another instance of the scheme on the | herbelin | 2009-11-08 |
| * | Restructuration of command.ml + generic infrastructure for inductive schemes | herbelin | 2009-11-08 |
| * | Fixed incorrect optimization in Prettyp.pr_located_qualid introduced | herbelin | 2009-08-07 |
| * | - Fixing #2090 (occur check missing when trying to solve evar-evar equation). | herbelin | 2009-04-25 |
| * | - Structuring Numbers and fixing Setoid in stdlib's doc. | herbelin | 2009-01-19 |
| * | Propagating commit 11343 from branch v8.2 to trunk (wish 1934 about | herbelin | 2008-09-02 |
| * | - Extension de "generalize" en "generalize c as id at occs". | herbelin | 2008-06-08 |
| * | - Add pretty-printers for Idpred, Cpred and transparent_state, used for | msozeau | 2008-04-24 |
| * | Prise en compte des coercions dans les clauses "with" même si le type | herbelin | 2008-04-23 |
| * | Bugs, nettoyage, et améliorations diverses | herbelin | 2008-04-13 |
| * | Ocaml toplevel convenience. | glondu | 2007-12-07 |
| * | - Correction bug dans syntaxe des match (liste de motifs vide était acceptée) | herbelin | 2007-08-22 |
| * | Export de l'afficheur de substitutions de noms de modules pour le débogueur | herbelin | 2007-01-19 |
| * | PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifier | herbelin | 2006-05-23 |
| * | Ajout printer Idset.t | herbelin | 2006-01-29 |
| * | Restructuration et simplification des fonctions d'affichage, de détypage | herbelin | 2006-01-11 |
| * | Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés) | herbelin | 2006-01-04 |
| * | MAJ restructuration constrintern.ml | herbelin | 2005-12-23 |
| * | Ajout constant printer | herbelin | 2005-02-18 |
Hugo Herbelin
Matthieu Sozeau
Pierre Boutillier
Pierre Letouzey
Arnaud Spiwack
aspiwack
letouzey
msozeau
herbelin
pboutill
glondu