aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Arith: full integration of the "Numbers" modular frameworkGravatar Pierre Letouzey2014-07-09
* Fixing bug #3270. Patch by Robbert Krebbers.Gravatar Pierre-Marie Pédrot2014-07-08
* Move Params definition in generalize rewriting out of a section so thatGravatar Matthieu Sozeau2014-06-29
* Avoid using a deprecated lemma in the standard library.Gravatar Guillaume Melquiond2014-06-26
* Remove some theories that have been deprecated for 10 years.Gravatar Guillaume Melquiond2014-06-26
* Export the right modules in Setoid, avoiding anomalies in generalized rewriting.Gravatar Matthieu Sozeau2014-06-26
* Deactivate the "Standard Propositions Naming" flag, source of a lot ofGravatar Hugo Herbelin2014-06-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-27 10:21:41 +0000