aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/lemmas.ml
Commit message (Expand)AuthorAge
* Revert "Add [Polymorphic] flag for defs"Gravatar msozeau2011-04-13
* - Remove create_evar_defsGravatar msozeau2011-04-13
* Add [Polymorphic] flag for defsGravatar msozeau2011-04-13
* Lazy loading of opaque proofs: fast as -dont-load-proofs without its drawbacksGravatar letouzey2011-04-03
* Interp a definition with the implicit arguments of its local contextGravatar pboutill2011-02-10
* A fine-grain control of inlining at functor application via priority levelsGravatar letouzey2011-01-31
* Remove the "Boxed" syntaxes and the const_entry_boxed fieldGravatar letouzey2011-01-28
* Minor factorization of the part of the code used for Unnamed_thm saving.Gravatar herbelin2010-10-31
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Made tclABSTRACT normalize evars before saying it does not supportGravatar herbelin2010-06-29
* Automatic introduction of names given before ":" in Lemma's andGravatar herbelin2010-06-09
* - Fixing bug #2308 about Lemma ... withGravatar vsiles2010-05-04
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Granting wish #2249 (checking existing lemma name also when in a section).Gravatar herbelin2010-04-09
* Fixed bug #2260 (check of resolution of all evars in the declarationGravatar herbelin2010-03-24
* Added support for definition of fixpoints using tactics.Gravatar herbelin2009-11-27
* A bit of cleaning around name generation + creation of dedicated file namegen.mlGravatar herbelin2009-11-09
* Restructuration of command.ml + generic infrastructure for inductive schemesGravatar herbelin2009-11-08
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 17:50:07 +0000