aboutsummaryrefslogtreecommitdiff
path: root/dev/base_include
AgeCommit message (Expand)Author
2012-10-16Split Tacinterp in 3 files : Tacsubst, Tacintern and Tacinterpletouzey
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-05-29Strongly reduce the dependencies of grammar.cma, modulo two hacksletouzey
2012-04-12lib directory is cut in 2 cma.pboutill
2012-04-06Removing Dhyp from debugger.herbelin
2012-03-14Everything compiles again.msozeau
2012-02-01Debugger vs tracer: Two different behaviors wrt printing: The debuggerherbelin
2011-10-15dev/base_include: display a nice message at the end of the loadletouzey
2011-04-26dev/base_include: no more mod_self_idletouzey
2011-04-13- Remove create_evar_defsmsozeau
2011-04-06Fix dev/base_include after change of constant_bodyletouzey
2010-12-23Rename rawterm.ml into glob_term.mlglondu
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2010-06-18Quick fix for having clenv debug printer working in trunk.herbelin
2010-04-22Here comes the commit, announced long ago, of the new tactic engine.aspiwack
2009-11-09A bit of cleaning around name generation + creation of dedicated file namegen.mlherbelin
2009-11-08Fixed "Scheme Equality" when another instance of the scheme on theherbelin
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-08-07Fixed incorrect optimization in Prettyp.pr_located_qualid introducedherbelin
2009-04-25- Fixing #2090 (occur check missing when trying to solve evar-evar equation).herbelin
2009-01-19- Structuring Numbers and fixing Setoid in stdlib's doc.herbelin
2008-09-02Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutherbelin
2008-06-08- Extension de "generalize" en "generalize c as id at occs".herbelin
2008-04-24- Add pretty-printers for Idpred, Cpred and transparent_state, used formsozeau
2008-04-23Prise en compte des coercions dans les clauses "with" même si le typeherbelin
2008-04-13Bugs, nettoyage, et améliorations diversesherbelin
2007-12-07Ocaml toplevel convenience.glondu
2007-08-22- Correction bug dans syntaxe des match (liste de motifs vide était acceptée)herbelin
2007-01-19Export de l'afficheur de substitutions de noms de modules pour le débogueurherbelin
2006-05-23PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierherbelin
2006-01-29Ajout printer Idset.therbelin
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2006-01-04Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)herbelin
2005-12-23MAJ restructuration constrintern.mlherbelin
2005-02-18Ajout constant printerherbelin
2005-01-02Découpage des printers pour ne pas avoir de dépendances en la vm dans les p...herbelin
2004-12-29Ajout printer bigintherbelin
2004-11-12Changement dans les boxed values .gregoire
2004-10-20COMMITED BYTECODE COMPILERbarras
2003-04-07Ajout translateherbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2001-08-10Parsingherbelin
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
2001-05-15Modification pour passage p-automatesmohring
2001-05-10ajout d'un afficher de contexte et d'une fonction constbody_of_stringletouzey
2001-04-03Make sure that the COQTOP variable is really used, when it is set.bertot
2000-12-15Printermohring