aboutsummaryrefslogtreecommitdiffhomepage
path: root/library/assumptions.ml
Commit message (Expand)AuthorAge
* Assumptions: more informative print for False axiom (Close: #4054)Gravatar Enrico Tassi2015-06-29
* Tentative fix for bug #4078.Gravatar Pierre-Marie Pédrot2015-02-21
* More resilient implementation of Print Assumptions.Gravatar Pierre-Marie Pédrot2015-02-21
* Fixing bug #4053.Gravatar Pierre-Marie Pédrot2015-02-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Grammar: "avoiding to" isn't proper, eitherGravatar Jason Gross2014-08-25
* Initial work on reintroducing old-style polymorphism for compatibility (the s...Gravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Declarations.mli: reorganization of modular structuresGravatar letouzey2013-08-20
* Revised infrastructure for lazy loading of opaque proofsGravatar letouzey2013-04-02
* kernel/declarations becomes a pure mliGravatar letouzey2013-02-26
* Names: revised representation of constants and mutual_inductiveGravatar letouzey2013-02-19
* Uniformization of the "anomaly" command.Gravatar ppedrot2013-01-28
* Modulification of LabelGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Monomorphization (library)Gravatar ppedrot2012-11-22
* Fixed #2926:Gravatar ppedrot2012-10-29
* Partial revert of Yann commit in order to use CLib.List when openingGravatar ppedrot2012-09-14
* This patch removes unused "open" (automatically generated fromGravatar regisgia2012-09-14
* Updating headers.Gravatar herbelin2012-08-08
* Module names and constant/inductive names are now in two separate namespacesGravatar letouzey2012-03-26
* Noise for nothingGravatar pboutill2012-03-02
* First attempt at making Print Assumption compatible with opaque modules (fix ...Gravatar letouzey2011-10-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-24 12:37:53 +0000