aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2014-08-26Prove forall extensionalityJason Gross
2014-08-26sed s'/_one_var/_on/g'Jason Gross
2014-08-26Generalize EqdepFactsJason Gross
2014-08-25"allows to", like "allowing to", is improperJason Gross
2014-08-25instanciation is French, instantiation is EnglishJason Gross
2014-08-25Grammar: "allowing to" is not proper EnglishJason Gross
2014-08-18Adding a new intro-pattern for "apply in" on the fly. Using syntaxHugo Herbelin
2014-08-18Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toHugo Herbelin
2014-08-12A couple of fixes/improvements in -beautify, but backtracking onHugo Herbelin
2014-08-07Instead of relying on a trick to make the constructor tactic parse, putPierre-Marie Pédrot
2014-08-07Removing the "constructor" tactic from the AST.Pierre-Marie Pédrot
2014-08-05Improving printing of "[]" (nil) in spite of the risk of collisionHugo Herbelin
2014-08-05Testing beautifying on an example.Hugo Herbelin
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-31 08:18:56 +0000