aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/indschemes.ml
Commit message (Expand)AuthorAge
* More uniformisation in Pp.warn functions.Gravatar ppedrot2012-05-30
* global_reference migrated from Libnames to new Globnames, less deps in gramma...Gravatar letouzey2012-05-29
* Noise for nothingGravatar pboutill2012-03-02
* Deactivated automatic inference of _case schemes, as it was in 8.3Gravatar herbelin2011-12-17
* A pass on warning printings. Made systematic the use of msg_warning soGravatar herbelin2011-12-17
* Proof using ...Gravatar gareuselesinge2011-12-12
* Added a DEPRECATED flag in declaration of options. For now only two options a...Gravatar ppedrot2011-11-24
* Another bug of Scheme Induction (generated names dep/nodep were swapped).Gravatar herbelin2011-06-13
* Fixing an anomaly in Scheme Induction.Gravatar herbelin2011-06-13
* turn the automatic generation of boolean equalityGravatar vsiles2011-05-16
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Remove obsolete TheoryListGravatar glondu2011-02-10
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* * 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
* Added a new exception for already declared Schemes, Gravatar vsiles2010-04-27
* Fixes in rewrite and a Elimination/Case to Scheme:Gravatar msozeau2010-03-06
* Minor fixes.Gravatar msozeau2010-03-05
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
* Quick fix for restoring a left-to-right rewriting lemma compatibleGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08