aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/base_include
Commit message (Expand)AuthorAge
* Update debug code according to reorganization into modules.Gravatar msozeau2013-02-27
* Adapt dev/base_include to new DeclarationsGravatar letouzey2013-02-27
* Added Evarsolve to the list of modules to open for debugging.Gravatar herbelin2013-02-21
* Split Tacinterp in 3 files : Tacsubst, Tacintern and TacinterpGravatar letouzey2012-10-16
* place all pretty-printing files in new dir printing/Gravatar letouzey2012-05-29
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Strongly reduce the dependencies of grammar.cma, modulo two hacksGravatar letouzey2012-05-29
* lib directory is cut in 2 cma.Gravatar pboutill2012-04-12
* Removing Dhyp from debugger.Gravatar herbelin2012-04-06
* Everything compiles again.Gravatar msozeau2012-03-14
* Debugger vs tracer: Two different behaviors wrt printing: The debuggerGravatar herbelin2012-02-01
* dev/base_include: display a nice message at the end of the loadGravatar letouzey2011-10-15
* dev/base_include: no more mod_self_idGravatar letouzey2011-04-26
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Fix dev/base_include after change of constant_bodyGravatar letouzey2011-04-06
* Rename rawterm.ml into glob_term.mlGravatar glondu2010-12-23
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Quick fix for having clenv debug printer working in trunk.Gravatar herbelin2010-06-18
* Here comes the commit, announced long ago, of the new tactic engine.Gravatar aspiwack2010-04-22
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Fixed "Scheme Equality" when another instance of the scheme on theGravatar herbelin2009-11-08
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Fixed incorrect optimization in Prettyp.pr_located_qualid introducedGravatar herbelin2009-08-07
* - Fixing #2090 (occur check missing when trying to solve evar-evar equation).Gravatar herbelin2009-04-25
* - Structuring Numbers and fixing Setoid in stdlib's doc.Gravatar herbelin2009-01-19
* Propagating commit 11343 from branch v8.2 to trunk (wish 1934 aboutGravatar herbelin2008-09-02
* - Extension de "generalize" en "generalize c as id at occs".Gravatar herbelin2008-06-08
* - Add pretty-printers for Idpred, Cpred and transparent_state, used forGravatar msozeau2008-04-24
* Prise en compte des coercions dans les clauses "with" même si le typeGravatar herbelin2008-04-23
* Bugs, nettoyage, et améliorations diversesGravatar herbelin2008-04-13
* Ocaml toplevel convenience.Gravatar glondu2007-12-07
* - Correction bug dans syntaxe des match (liste de motifs vide était acceptée)Gravatar herbelin2007-08-22
* Export de l'afficheur de substitutions de noms de modules pour le débogueurGravatar herbelin2007-01-19
* PÃréouverture de la plupart des fichis pour éviter d'avoir à qualifierGravatar herbelin2006-05-23
* Ajout printer Idset.tGravatar herbelin2006-01-29
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Affichage concis des locations (si jamais ppterm/pprawterm sont débranchés)Gravatar herbelin2006-01-04
* MAJ restructuration constrintern.mlGravatar herbelin2005-12-23
* Ajout constant printerGravatar herbelin2005-02-18
* Découpage des printers pour ne pas avoir de dépendances en la vm dans les p...Gravatar herbelin2005-01-02
* Ajout printer bigintGravatar herbelin2004-12-29
* Changement dans les boxed values .Gravatar gregoire2004-11-12
* COMMITED BYTECODE COMPILERGravatar barras2004-10-20
* Ajout translateGravatar herbelin2003-04-07
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02
* petits changements cosmetiques sur les tactiquesGravatar barras2002-02-15
* ParsingGravatar herbelin2001-08-10
* amelioration des messages d'erreurs vis a vis des evarsGravatar barras2001-05-23
* Modification pour passage p-automatesGravatar mohring2001-05-15