aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/elimschemes.ml
Commit message (Expand)AuthorAge
* Getting rid of AUContext abstraction breakers in Elimschemes.Gravatar Pierre-Marie Pédrot2017-07-13
* Safe API for accessing universe constraints of global references.Gravatar Pierre-Marie Pédrot2017-07-11
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* Squashed commit of the following:Gravatar Amin Timany2017-06-16
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
|\
| * Fix #4769, univ poly and elim schemes in sectionsGravatar Matthieu Sozeau2016-07-29
* | primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
* | Removing some goal unsafeness in inductive schemes.Gravatar Pierre-Marie Pédrot2015-10-29
|/
* 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-27 04:58:08 +0000