aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Cleanup treatment of template universe polymorphism (thanks to E. TassiGravatar Matthieu Sozeau2014-06-20
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Make standard library independent of the names generated byGravatar Hugo Herbelin2014-06-04
* Small lemma about Relations.Gravatar Hugo Herbelin2014-06-04
* Remove spurious Show in script.Gravatar Matthieu Sozeau2014-06-04
* Making those proofs which depend on names generated for the argumentsGravatar Hugo Herbelin2014-06-01
* Basic lemmas about the algebraic structure of equality.Gravatar Hugo Herbelin2014-05-31
* Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qGravatar Pierre Boutillier2014-05-26
* - Fix in kernel conversion not folding the universe constraintsGravatar Matthieu Sozeau2014-05-26
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Revert "Fix Qcanon after changes on injection."Gravatar Maxime Dénès2014-05-18
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* Now parsing rules of ML-declared tactics are only made available after theGravatar Pierre-Marie Pédrot2014-05-12
* Update and start testing rewrite-in-type code.Gravatar Matthieu Sozeau2014-05-09
* Restore implicit arguments of irreflexivity (fixes bug #3305).Gravatar Matthieu Sozeau2014-05-09
* Removing comment outdated since eta holds in conversion rule (thisGravatar Hugo Herbelin2014-05-07
* Fix after merge.Gravatar Matthieu Sozeau2014-05-06
* - Fix treatment of global universe constraints which should be passed alongGravatar Matthieu Sozeau2014-05-06
* Try a new way of handling template universe levelsGravatar Matthieu Sozeau2014-05-06
* - Fix arity handling in retyping (de Bruijn bug!)Gravatar Matthieu Sozeau2014-05-06
* - 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
* Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Gravatar Matthieu Sozeau2014-05-06
* Restore reasonable performance by not allocating during universe checks,Gravatar Matthieu Sozeau2014-05-06
* - Rename eq to equal in Univ, document new modules, set interfaces.Gravatar Matthieu Sozeau2014-05-06
* Correct rebase on STM code. Thanks to E. Tassi for help on dealing withGravatar Matthieu Sozeau2014-05-06
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Pos.iter arguments in a better order for cbn.Gravatar Pierre Boutillier2014-05-02
* Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentGravatar Pierre Boutillier2014-05-02
* Eta contractions to please cbnGravatar Pierre Boutillier2014-05-02
* Fix Qcanon after changes on injection.Gravatar Maxime Dénès2014-04-30
* Import proof of decidability of negated formulas from Coquelicot.Gravatar Guillaume Melquiond2014-04-23
* Remove some uses of excluded middle.Gravatar Guillaume Melquiond2014-04-22
* Replace the proof of sig_forall_dec from Kaliszyk/O'Connor by the one from Co...Gravatar Guillaume Melquiond2014-04-22
* Fixing missing headers.Gravatar Hugo Herbelin2014-04-16
* No more Coersion in Init.Gravatar Pierre Boutillier2014-04-10
* Define [projT3] and [proj3_sig]Gravatar Jason Gross2014-04-10
* Closing bug #3164Gravatar Julien Forest2014-04-04
* Add missing lemmas: Rplus_eq_compat_r and Rplus_eq_reg_r.Gravatar Guillaume Melquiond2014-03-10
* Pos.compare_cont takes the comparison as first argumentGravatar Pierre Boutillier2014-02-28
* fixup complement FinGravatar Pierre Boutillier2014-02-24
* Less dependencies in Omega.Gravatar Pierre-Marie Pédrot2014-02-08
* FinFun.v: results about injective/surjective/bijective fonctions over finite ...Gravatar Pierre Letouzey2014-02-07
* [Coercion]s use [Sortclass], not [Prop] (in docs)Gravatar Jason Gross2014-01-24
* List: Bug 3039 weaker requirement for fold symmetricGravatar Pierre Boutillier2013-12-20
* Better unification for [projT1] and [proj1_sig].Gravatar Jason Gross2013-12-12
* Generalize eq_proofs_unicityGravatar Jason Gross2013-12-12
* Improved the presentation of the proof of UIP_refl_nat.Gravatar Hugo Herbelin2013-12-04
* Add lemma derivable_pt_lim_atan.Gravatar Guillaume Melquiond2013-12-04
* Fix statement of Rplus_lt_reg_r and add Rplus_lt_reg_l.Gravatar Guillaume Melquiond2013-12-03
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-03 06:07:20 +0000