aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Move to a representation of universe polymorphic constants using indices for ...Gravatar Matthieu Sozeau2014-08-03
* Adding a generalized version of fold_Equal to FMapFacts.Gravatar Pierre Courtieu2014-07-31
* Simplified rect2, it turns out Arthur's trick was not required.Gravatar Maxime Dénès2014-07-22
* A version of Fin.rect2 that is compatible with the fix of the guard condition.Gravatar Maxime Dénès2014-07-22
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
* Completing c236b51348d2 by fixing EqdepFactsv actually committing theGravatar Hugo Herbelin2014-07-17
* Added a (constructive) proof of Weak Konig's lemma for decidable trees.Gravatar Hugo Herbelin2014-07-15
* Some basics facts about eq_dep.Gravatar Hugo Herbelin2014-07-15
* MSetRBT: unfortunate typo in compare_height (fix #3413)Gravatar Pierre Letouzey2014-07-10
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 18:49:13 +0000