aboutsummaryrefslogtreecommitdiffhomepage
path: root/stm/lemmas.ml
Commit message (Expand)AuthorAge
* When typechecking a lemma statement, try to resolve typeclasses beforeGravatar Matthieu Sozeau2015-10-14
* Univs: fix semantics of Type in proof mode in universe-polymorphic modeGravatar Matthieu Sozeau2015-10-02
* Univs: fix handling of side effects/delayed proofsGravatar Matthieu Sozeau2015-10-02
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Univs: Add universe binding lists to definitionsGravatar Matthieu Sozeau2015-09-14
* Removing code duplication in Lemmas.Gravatar Pierre-Marie Pédrot2015-08-19
* Fixing what seems to be a typo.Gravatar Hugo Herbelin2015-07-29
* Admitted does not drop poly-univ constraints (Fix #4244)Gravatar Enrico Tassi2015-06-03
* Fix bug #4159Gravatar Matthieu Sozeau2015-05-27
* admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)Gravatar Enrico Tassi2015-03-11
* Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
* Update headers.Gravatar Maxime Dénès2015-01-12
* Vi2vo: fix handling of univ constraints coming from the bodyGravatar Enrico Tassi2014-12-23
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Fix backtracking issue in Defined (Close 3780)Gravatar Enrico Tassi2014-10-30
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Lemmas/Pfedit: use full evar_map instead of universe contexts to start proofs.Gravatar Arnaud Spiwack2014-10-22
* STM: simplify how the term part of a side effect is retrievedGravatar Enrico Tassi2014-10-13
* library/opaqueTables: enable their use in interactive modeGravatar Enrico Tassi2014-10-13
* Uniformisation of the order of arguments env and sigma.Gravatar Hugo Herbelin2014-09-12
* Print [Variant] types with the keyword [Variant].Gravatar Arnaud Spiwack2014-09-04
* Fixing universe substitution in mutual fixpoints.Gravatar Pierre-Marie Pédrot2014-07-16
* Better handling of the universe context in case of Admitted proof obligations.Gravatar Matthieu Sozeau2014-07-10
* all coqide specific files moved into ide/Gravatar Enrico Tassi2014-06-25
* Fix handling of side effects in Defined objects (Closes: HoTT#111 + 3344)Gravatar Enrico Tassi2014-06-23
* Proofs now take and return an evar_universe_context, simplifying interfacesGravatar Matthieu Sozeau2014-06-18
* Moving hook code from Future to Lemmas. This seemed to disrupt compilation ofGravatar Pierre-Marie Pédrot2014-06-08
* Enforce a correct exception handling in declaration_hooksGravatar Enrico Tassi2014-06-08
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* - Fix bug preventing apply from unfolding Fixpoints.Gravatar Matthieu Sozeau2014-05-06
* Adapt universe polymorphic branch to new handling of futures for delayed proofs.Gravatar Matthieu Sozeau2014-05-06
* Lemmas: export standard proof terminatorGravatar Enrico Tassi2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* Rework handling of universes on top of the STM, allowing for delayedGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Adding a stm/ folder, as asked during last workgroup. It was essentially movingGravatar Pierre-Marie Pédrot2014-04-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 15:09:35 +0000