aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2014-11-02Supporting "at occs" as a short-hand for "in |- * at occs" in "destruct".Hugo Herbelin
2014-10-27Make sure that Logic/ExtensionalityFacts gets compiled.Guillaume Melquiond
2014-10-27Fix some typos.Guillaume Melquiond
2014-10-27Fix some typos in comments.Guillaume Melquiond
2014-10-22EqdepFacts: generalize statements which were wrongly restricted to Prop.Arnaud Spiwack
2014-10-22Fixing typo absorption (bug #3751).Hugo Herbelin
2014-10-17Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...Hugo Herbelin
2014-10-17Essai où assert_style n'est utilisé que si pas visuellement une équation;Hugo Herbelin
2014-10-16ConstructiveEpsilon: simplify the before_witness type using non-uniform param...Arnaud Spiwack
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
2014-10-10Fix segfault in native compiler on int31 division.Maxime Dénès
2014-10-01eta contractionsPierre Boutillier
2014-10-01argument flip of Cyclic31.nshiftr and Cyclic31.nshiftlPierre Boutillier
2014-10-01Simpl less (so that cbn will not simpl too much)Pierre Boutillier
2014-09-27Keyed unification option, compiling the whole standard libraryMatthieu Sozeau
2014-09-26Hurkens.v: Fix a syntax error.Arnaud Spiwack
2014-09-26ClassicalFacts: adds a proof that weak excluded middle implies weak proof irr...Arnaud Spiwack
2014-09-26Hurkens.v: new paradox: type of modal propositions is not a retract.Arnaud Spiwack
2014-09-26Hurkens.v: fix coqdoc formatting in a comment.Arnaud Spiwack
2014-09-25Hurkens.v: update comments.Arnaud Spiwack
2014-09-24Return a Prop not an arbitrary Type, and correct a typo.Matthieu Sozeau
2014-09-24Hurkens.v: show proofs in coqdoc.Arnaud Spiwack
2014-09-24Hurkens.v: a proof of [Type@{i}<>A] for any [A:Type@{i}].Arnaud Spiwack
2014-09-24Hurkens.v: coqdoc documentation.Arnaud Spiwack
2014-09-24A new version of Hurkens.v.Arnaud Spiwack
2014-09-23adds general facts in the Reals library, whose need was detected inYves Bertot
2014-09-17Change some Defined into Qed.Guillaume Melquiond
2014-09-17Add some missing Proof statements.Guillaume Melquiond
2014-09-17Change an axiom into a definition.Guillaume Melquiond
2014-09-09- Fix printing and parsing of primitive projections, including the SetMatthieu Sozeau
2014-09-08Removing the XML plugin.Pierre-Marie Pédrot
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-10-14 21:09:55 +0000