aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Adds two lemmas about hderror to the List standard library.Gravatar Sébastien Hinderer2014-12-18
* Implement the nodup function on lists and prove associated results.Gravatar Sébastien Hinderer2014-12-18
* Lists: enhanced version of Seb's last commit on Exists/ForallGravatar Pierre Letouzey2014-12-18
* Lists: a few results on Exists and Forall and a bit of code cleanup.Gravatar Sébastien Hinderer2014-12-18
* Failing on unbound notation variable in notation level modifiersGravatar Hugo Herbelin2014-12-15
* List.v: sequel to Sebastien's commit (some cosmetics + a few shorter proofs)Gravatar Pierre Letouzey2014-12-11
* First series of results on lists.Gravatar Sébastien Hinderer2014-12-11
* Added an arithmetical characterization of the hypothesis of WKL.Gravatar Hugo Herbelin2014-12-01
* Clarifying the role of ListSet.v in the library, compared to otherGravatar Hugo Herbelin2014-11-18
* Enforcing a stronger difference between the two syntaxes "simplGravatar Hugo Herbelin2014-11-16
* Improving elimination with indices, getting rid of intrusive residualGravatar Hugo Herbelin2014-11-02
* Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Gravatar Hugo Herbelin2014-11-02
* Make sure that Logic/ExtensionalityFacts gets compiled.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos.Gravatar Guillaume Melquiond2014-10-27
* Fix some typos in comments.Gravatar Guillaume Melquiond2014-10-27
* EqdepFacts: generalize statements which were wrongly restricted to Prop.Gravatar Arnaud Spiwack2014-10-22
* Fixing typo absorption (bug #3751).Gravatar Hugo Herbelin2014-10-22
* Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Gravatar Hugo Herbelin2014-10-17
* Essai où assert_style n'est utilisé que si pas visuellement une équation;Gravatar Hugo Herbelin2014-10-17
* ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Gravatar Arnaud Spiwack2014-10-16
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
* Fix segfault in native compiler on int31 division.Gravatar Maxime Dénès2014-10-10
* eta contractionsGravatar Pierre Boutillier2014-10-01
* argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlGravatar Pierre Boutillier2014-10-01
* Simpl less (so that cbn will not simpl too much)Gravatar Pierre Boutillier2014-10-01
* Keyed unification option, compiling the whole standard libraryGravatar Matthieu Sozeau2014-09-27
* Hurkens.v: Fix a syntax error.Gravatar Arnaud Spiwack2014-09-26
* ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: new paradox: type of modal propositions is not a retract.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: fix coqdoc formatting in a comment.Gravatar Arnaud Spiwack2014-09-26
* Hurkens.v: update comments.Gravatar Arnaud Spiwack2014-09-25
* Return a Prop not an arbitrary Type, and correct a typo.Gravatar Matthieu Sozeau2014-09-24
* Hurkens.v: show proofs in coqdoc.Gravatar Arnaud Spiwack2014-09-24
* Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Gravatar Arnaud Spiwack2014-09-24
* Hurkens.v: coqdoc documentation.Gravatar Arnaud Spiwack2014-09-24
* A new version of Hurkens.v.Gravatar Arnaud Spiwack2014-09-24
* adds general facts in the Reals library, whose need was detected inGravatar Yves Bertot2014-09-23
* Change some Defined into Qed.Gravatar Guillaume Melquiond2014-09-17
* Add some missing Proof statements.Gravatar Guillaume Melquiond2014-09-17
* Change an axiom into a definition.Gravatar Guillaume Melquiond2014-09-17
* - Fix printing and parsing of primitive projections, including the SetGravatar Matthieu Sozeau2014-09-09
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Prove forall extensionalityGravatar Jason Gross2014-08-26
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-30 04:13:41 +0000