aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* sed s'/_one_var/_on/g'Gravatar Jason Gross2014-08-26
* Generalize EqdepFactsGravatar Jason Gross2014-08-26
* "allows to", like "allowing to", is improperGravatar Jason Gross2014-08-25
* instanciation is French, instantiation is EnglishGravatar Jason Gross2014-08-25
* Grammar: "allowing to" is not proper EnglishGravatar Jason Gross2014-08-25
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Factorizing cutrewrite (to be made obsolote) and dependent rewrite (toGravatar Hugo Herbelin2014-08-18
* A couple of fixes/improvements in -beautify, but backtracking onGravatar Hugo Herbelin2014-08-12
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Improving printing of "[]" (nil) in spite of the risk of collisionGravatar Hugo Herbelin2014-08-05
* Testing beautifying on an example.Gravatar Hugo Herbelin2014-08-05
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Testing a replacement of "cut" by "enough" on a couple of test files.Gravatar Hugo Herbelin2014-08-05
* More proofs independent of the names generated by induction/elim overGravatar Hugo Herbelin2014-08-05
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 19:38:26 +0000