aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2014-08-05Experimentally adding an option for automatically erasing anHugo Herbelin
2014-08-05Testing a replacement of "cut" by "enough" on a couple of test files.Hugo Herbelin
2014-08-05More proofs independent of the names generated by induction/elim overHugo Herbelin
2014-08-03Move to a representation of universe polymorphic constants using indices for ...Matthieu Sozeau
2014-07-31Adding a generalized version of fold_Equal to FMapFacts.Pierre Courtieu
2014-07-22Simplified rect2, it turns out Arthur's trick was not required.Maxime Dénès
2014-07-22A version of Fin.rect2 that is compatible with the fix of the guard condition.Maxime Dénès
2014-07-22Fixed proof of irrelevance of le on nat, inspired by theMaxime Dénès
2014-07-17Completing c236b51348d2 by fixing EqdepFactsv actually committing theHugo Herbelin
2014-07-15Added a (constructive) proof of Weak Konig's lemma for decidable trees.Hugo Herbelin
2014-07-15Some basics facts about eq_dep.Hugo Herbelin
2014-07-10MSetRBT: unfortunate typo in compare_height (fix #3413)Pierre Letouzey
2014-07-09Arith: full integration of the "Numbers" modular frameworkPierre Letouzey
2014-07-08Fixing bug #3270. Patch by Robbert Krebbers.Pierre-Marie Pédrot
2014-06-29Move Params definition in generalize rewriting out of a section so thatMatthieu Sozeau
2014-06-26Avoid using a deprecated lemma in the standard library.Guillaume Melquiond
2014-06-26Remove some theories that have been deprecated for 10 years.Guillaume Melquiond
2014-06-26Export the right modules in Setoid, avoiding anomalies in generalized rewriting.Matthieu Sozeau
2014-06-26Deactivate the "Standard Propositions Naming" flag, source of a lot ofHugo Herbelin
2014-06-20Cleanup treatment of template universe polymorphism (thanks to E. TassiMatthieu Sozeau
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Make standard library independent of the names generated byHugo Herbelin
2014-06-04Small lemma about Relations.Hugo Herbelin
2014-06-04Remove spurious Show in script.Matthieu Sozeau
2014-06-01Making those proofs which depend on names generated for the argumentsHugo Herbelin
2014-05-31Basic lemmas about the algebraic structure of equality.Hugo Herbelin
2014-05-26Cbn reduces Pos.compare p~1 q~1 to Pos.compare p qPierre Boutillier
2014-05-26- Fix in kernel conversion not folding the universe constraintsMatthieu Sozeau
2014-05-20Moving (e)transitivity out of the AST.Pierre-Marie Pédrot
2014-05-18Revert "Fix Qcanon after changes on injection."Maxime Dénès
2014-05-16Moving argument-free tactics out of the AST into a dedicatedPierre-Marie Pédrot
2014-05-12Now parsing rules of ML-declared tactics are only made available after thePierre-Marie Pédrot
2014-05-09Update and start testing rewrite-in-type code.Matthieu Sozeau
2014-05-09Restore implicit arguments of irreflexivity (fixes bug #3305).Matthieu Sozeau
2014-05-07Removing comment outdated since eta holds in conversion rule (thisHugo Herbelin
2014-05-06Fix after merge.Matthieu Sozeau
2014-05-06- Fix treatment of global universe constraints which should be passed alongMatthieu Sozeau
2014-05-06Try a new way of handling template universe levelsMatthieu Sozeau
2014-05-06- Fix arity handling in retyping (de Bruijn bug!)Matthieu Sozeau
2014-05-06- Fix bug preventing apply from unfolding Fixpoints.Matthieu Sozeau
2014-05-06Adapt universe polymorphic branch to new handling of futures for delayed proofs.Matthieu Sozeau
2014-05-06Fix issue #88: restrict_universe_context was wrongly forgetting about constra...Matthieu Sozeau
2014-05-06Restore reasonable performance by not allocating during universe checks,Matthieu Sozeau
2014-05-06- Rename eq to equal in Univ, document new modules, set interfaces.Matthieu Sozeau
2014-05-06Correct rebase on STM code. Thanks to E. Tassi for help on dealing withMatthieu Sozeau
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-05-02Pos.iter arguments in a better order for cbn.Pierre Boutillier
2014-05-02Cbn is happier when ?SetPositive fixpoints have the set as recursive argumentPierre Boutillier
2014-05-02Eta contractions to please cbnPierre Boutillier
2014-04-30Fix Qcanon after changes on injection.Maxime Dénès
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:43:53 +0000