aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elimschemes.ml
Commit message (Expand)AuthorAge
* Avoid type checking private_constants (side_eff) again during Qed (#4357).Gravatar Enrico Tassi2015-10-28
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-09-23
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Reverting 16 last commits, committed mistakenly using the wrong push command.Gravatar Hugo Herbelin2015-08-02
* Give a way to control if the decidable-equality schemes are built likeGravatar Hugo Herbelin2015-08-02
* Make native compiler handle universe polymorphic definitions.Gravatar Maxime Dénès2015-01-17
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fix elimschemes accessing directly the universe context of inductives (fixes ...Gravatar Matthieu Sozeau2014-08-14
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Remove some more "open" and dead code thanks to OCaml4 warningsGravatar letouzey2012-10-02
* Updating headers.Gravatar herbelin2012-08-08
* Fixing discriminate for identity.Gravatar herbelin2011-05-26
* Some dead code removal, thanks to Oug analyzerGravatar letouzey2010-09-24
* Updated all headers for 8.3 and trunkGravatar herbelin2010-07-24
* Remove the svn-specific $Id$ annotationsGravatar letouzey2010-04-29
* Made the side-conditions of lemmas always come last when chaining "apply in"Gravatar herbelin2009-12-13
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-22 23:19:57 +0000