aboutsummaryrefslogtreecommitdiffhomepage
path: root/dev/include
Commit message (Expand)AuthorAge
* Adding econstr printer to "include" file.Gravatar Hugo Herbelin2017-07-12
* Fix a bug in cumulativityGravatar Amin Timany2017-06-16
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Adding a printer for Proof.proof reflecting the focusing layout.Gravatar Hugo Herbelin2017-01-26
* FIX: dev/includeGravatar Matej Kosik2016-11-05
* A fix to dev/include.Gravatar Hugo Herbelin2016-08-17
* More printers in tracer.Gravatar Hugo Herbelin2014-12-05
* Adding printers for ppproofview.Gravatar Hugo Herbelin2014-10-13
* Adding printer for named_context_val and Goal.goal in debugger.Gravatar Hugo Herbelin2014-10-09
* Adding a printer for hints.Gravatar Hugo Herbelin2014-10-07
* Debug RAKAMGravatar Pierre Boutillier2014-08-26
* - Fix bug #3368, due to wrong use of the Cst_stack for projections.Gravatar Matthieu Sozeau2014-06-11
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* print futures in caml toplevel tooGravatar Enrico Tassi2014-04-25
* Set officially the minimal OCaml requirement to 3.12.1Gravatar Pierre Letouzey2014-03-02
* - install evar printer for debuggingGravatar msozeau2013-10-29
* At least made the evar type opaque! There are still 5 remaining unsafeGravatar ppedrot2013-09-18
* Fix for bug #3017: wrong handling of the unresolvability statusGravatar msozeau2013-04-03
* remove a warning after Drop about print_hint_dbGravatar letouzey2013-02-27
* Revert "Fixing include printers"Gravatar pboutill2012-08-05
* Fixing include printersGravatar ppedrot2012-08-03
* Suspending declaration of undefined debug printers.Gravatar herbelin2011-12-18
* Merge subinstances branch by me and Tom Prince.Gravatar msozeau2011-11-17
* debugging.txt: no more typing of #use "include" if using .ocamlinitGravatar letouzey2011-10-15
* Fix unification: detect invalid evar instantiations due to scoping earlier.Gravatar msozeau2011-08-04
* Fixed a "feature" of "inversion" and "dependent rewrite" revealed byGravatar herbelin2011-07-18
* Cleaning debugging printer relative to new proof engine. InGravatar herbelin2011-06-21
* Factorize code of rewrite to make way for a new implementation using theGravatar msozeau2011-02-07
* Change of nomenclature: rawconstr -> glob_constrGravatar glondu2010-12-23
* Remove useless ppevd (which is identical to ppevm)Gravatar glondu2009-11-13
* Improved the treatment of Local/Global options (noneffective Local onGravatar herbelin2009-10-25
* - Fixing declarative mode in presence of high use of Change_evars nodesGravatar herbelin2009-05-20
* Execute #rectypes directive in embedded OCaml toplevel...Gravatar glondu2008-11-19
* Hint for Debian users.Gravatar glondu2008-03-18
* Add printer for Pp.std_ppcmds...Gravatar msozeau2008-02-08
* Merged revisions 10358-10362,10365,10371-10373,10377,10383-10384,10394-10395,...Gravatar msozeau2007-12-31
* Ocaml toplevel convenience.Gravatar glondu2007-12-07
* Ajout de eelim, ecase, edestruct et einduction (expérimental).Gravatar herbelin2007-10-03
* mise a jour du nouveau ring et ajout du nouveau field, avant renommagesGravatar barras2006-09-26
* Restructuration et simplification des fonctions d'affichage, de détypageGravatar herbelin2006-01-11
* Suppression des parseurs et printeurs v7; suppression du traducteur (mcanisme...Gravatar herbelin2005-12-26
* restructuration des printers: proofs passe avant parsingGravatar barras2004-09-17
* unification encore...Gravatar barras2004-09-08
* prettyprint des constr_substituted + un wrapping de prglobal pour qu'il n'ech...Gravatar letouzey2003-04-16
* Ajout affichage fconstrGravatar herbelin2002-12-05
* ajout d'un printer pour les global_referenceGravatar letouzey2002-11-04
* Modules dans COQ\!\!\!\!Gravatar coq2002-08-02