aboutsummaryrefslogtreecommitdiff
path: root/toplevel/ind_tables.ml
AgeCommit message (Expand)Author
2014-08-30Simplify even further the declaration of primitive projections,Matthieu Sozeau
2014-08-28Change the way primitive projections are declared to the kernel.Matthieu Sozeau
2014-06-17Safer entry point of primitive projections in the kernel, now it does recognizeMatthieu Sozeau
2014-06-08ind_tables: always declare side effects (Closes: HOTT#110)Enrico Tassi
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Rework handling of universes on top of the STM, allowing for delayedMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2013-12-24Qed: feedback when type checking is doneEnrico Tassi
2013-10-24More monomorphic List.mem + List.assoc + ...letouzey
2013-10-24Turn many List.assoc into List.assoc_fletouzey
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
2013-04-22code simplifications concerning Summaryletouzey
2013-03-13Restrict (try...with...) to avoid catching critical exn (part 13)letouzey
2013-03-11Added a Local Definition vernacular command. This type of definitionppedrot
2013-01-22New implementation of the conversion test, using normalization by evaluation tomdenes
2012-12-14Modulification of identifierppedrot
2012-12-14Moved Stringset and Stringmap to String namespace.ppedrot
2012-12-13Using library string functions.ppedrot
2012-11-26Monomorphization (toplevel)ppedrot
2012-09-14As r15801: putting everything from Util.array_* to CArray.*.ppedrot
2012-08-08Updating headers.herbelin
2012-03-02Noise for nothingpboutill
2011-12-12Proof using ...gareuselesinge
2011-11-02Add type annotations around all calls to Libobject.declare_objectletouzey
2011-10-08Scheme names: Use unprobable names + ensure names do not hide existing namesherbelin
2011-04-13Revert "Add [Polymorphic] flag for defs"msozeau
2011-04-13Add [Polymorphic] flag for defsmsozeau
2011-01-28Remove the "Boxed" syntaxes and the const_entry_boxed fieldletouzey
2010-09-24Some dead code removal, thanks to Oug analyzerletouzey
2010-09-02* removed declare_constant and declare_internal_constant vsiles
2010-09-02v13392 port from v8.3 to trunk : correct message when defining inductive schemesvsiles
2010-07-24Updated all headers for 8.3 and trunkherbelin
2010-06-29change the flag "internal" in declare/ind_tables from bool tovsiles
2010-05-29New pass on inductive schemesherbelin
2010-04-29Remove the svn-specific $Id$ annotationsletouzey
2009-11-08Restructuration of command.ml + generic infrastructure for inductive schemesherbelin
2009-09-17Remove useless Liboject.export_function fieldglondu
2009-09-17Delete trailing whitespaces in all *.{v,ml*} filesglondu
2009-08-13Death of "survive_module" and "survive_section" (the first one washerbelin
2008-04-01Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientherbelin
2007-10-05 Added the automatic generation of the boolean equality if possible and thevsiles
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-28 14:10:17 +0000