aboutsummaryrefslogtreecommitdiff
path: root/dev/include
AgeCommit message (Expand)Author
2013-09-18At least made the evar type opaque! There are still 5 remaining unsafeppedrot
2013-04-03Fix for bug #3017: wrong handling of the unresolvability statusmsozeau
2013-02-27remove a warning after Drop about print_hint_dbletouzey
2012-08-05Revert "Fixing include printers"pboutill
2012-08-03Fixing include printersppedrot
2011-12-18Suspending declaration of undefined debug printers.herbelin
2011-11-17Merge subinstances branch by me and Tom Prince.msozeau
2011-10-15debugging.txt: no more typing of #use "include" if using .ocamlinitletouzey
2011-08-04Fix unification: detect invalid evar instantiations due to scoping earlier.msozeau
2011-07-18Fixed a "feature" of "inversion" and "dependent rewrite" revealed byherbelin
2011-06-21Cleaning debugging printer relative to new proof engine. Inherbelin
2011-02-07Factorize code of rewrite to make way for a new implementation using themsozeau
2010-12-23Change of nomenclature: rawconstr -> glob_constrglondu
2009-11-13Remove useless ppevd (which is identical to ppevm)glondu
2009-10-25Improved the treatment of Local/Global options (noneffective Local onherbelin
2009-05-20- Fixing declarative mode in presence of high use of Change_evars nodesherbelin
2008-11-19Execute #rectypes directive in embedded OCaml toplevel...glondu
2008-03-18Hint for Debian users.glondu
2008-02-08Add printer for Pp.std_ppcmds...msozeau
2007-12-31Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...msozeau
2007-12-07Ocaml toplevel convenience.glondu
2007-10-03Ajout de eelim, ecase, edestruct et einduction (expérimental).herbelin
2006-09-26mise a jour du nouveau ring et ajout du nouveau field, avant renommagesbarras
2006-01-11Restructuration et simplification des fonctions d'affichage, de détypageherbelin
2005-12-26Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...herbelin
2004-09-17restructuration des printers: proofs passe avant parsingbarras
2004-09-08unification encore...barras
2003-04-16prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...letouzey
2002-12-05Ajout affichage fconstrherbelin
2002-11-04ajout d'un printer pour les global_referenceletouzey
2002-08-02Modules dans COQ\!\!\!\!coq
2002-02-15petits changements cosmetiques sur les tactiquesbarras
2001-11-06Suppression des local_constraints, des ctxtty et du focus.clrenard
2001-09-30Ajout du printer de tactiques + modif du Dynamic ocamldelahaye
2001-05-10ajout d'un afficher de contexte et d'une fonction constbody_of_stringletouzey
2000-01-07Restructuration printer et parserherbelin
1999-12-12Ajout pp pattern et rawtermherbelin
1999-12-03renommage pour eviter pbm avec ocamldep (syntax error)filliatr