aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/ind_tables.ml
Commit message (Expand)AuthorAge
* Noise for nothingGravatar pboutill2012-03-02
* Proof using ...Gravatar gareuselesinge2011-12-12
* Add type annotations around all calls to Libobject.declare_objectGravatar letouzey2011-11-02
* Scheme names: Use unprobable names + ensure names do not hide existing namesGravatar herbelin2011-10-08
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* * removed declare_constant and declare_internal_constant Gravatar vsiles2010-09-02
* v13392 port from v8.3 to trunk : correct message when defining inductive schemesGravatar vsiles2010-09-02
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* change the flag "internal" in declare/ind_tables from bool toGravatar vsiles2010-06-29
* New pass on inductive schemesGravatar herbelin2010-05-29
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
* Remove useless Liboject.export_function fieldGravatar glondu2009-09-17
* Delete trailing whitespaces in all *.{v,ml*} filesGravatar glondu2009-09-17
* Death of "survive_module" and "survive_section" (the first one wasGravatar herbelin2009-08-13
* Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaientGravatar herbelin2008-04-01
* Added the automatic generation of the boolean equality if possible and theGravatar vsiles2007-10-05
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 20:42:24 +0000