aboutsummaryrefslogtreecommitdiff
path: root/library/assumptions.ml
AgeCommit message (Expand)Author
2015-06-29Assumptions: more informative print for False axiom (Close: #4054)Enrico Tassi
2015-02-21Tentative fix for bug #4078.Pierre-Marie Pédrot
2015-02-21More resilient implementation of Print Assumptions.Pierre-Marie Pédrot
2015-02-17Fixing bug #4053.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-13library/opaqueTables: enable their use in interactive modeEnrico Tassi
2014-08-25Grammar: "avoiding to" isn't proper, eitherJason Gross
2014-05-06Initial work on reintroducing old-style polymorphism for compatibility (the s...Matthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-04-02Revised infrastructure for lazy loading of opaque proofsletouzey
2013-02-26kernel/declarations becomes a pure mliletouzey
2013-02-19Names: revised representation of constants and mutual_inductiveletouzey
2013-01-28Uniformization of the "anomaly" command.ppedrot
2012-12-18Modulification of Labelppedrot
2012-12-14Modulification of identifierppedrot
2012-11-22Monomorphization (library)ppedrot
2012-10-29Fixed #2926:ppedrot
2012-09-14Partial revert of Yann commit in order to use CLib.List when openingppedrot
2012-09-14This patch removes unused "open" (automatically generated fromregisgia
2012-08-08Updating headers.herbelin
2012-03-26Module names and constant/inductive names are now in two separate namespacesletouzey
2012-03-02Noise for nothingpboutill
2011-10-25First attempt at making Print Assumption compatible with opaque modules (fix ...letouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 19:07:37 +0000