aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2017-09-06changed statements of Rpower_lt and Rle_power and addedYves Bertot
2017-09-03Addressing BZ#5713 (classical_left/classical_right artificially restricted).Hugo Herbelin
2017-08-29A little reorganization of notations + a fix to #5608.Hugo Herbelin
2017-08-21Ensuring all .v files end with a newline to make "sed -i" work better on them.Hugo Herbelin
2017-07-26Merge PR #882: Adding a V8.7 compatibility version number.Maxime Dénès
2017-07-26Merge PR #885: Removing a dummy parameter in some FMapPositive statements.Maxime Dénès
2017-07-26Merge PR #845: Add Z.mod_div lemma to standard library.Maxime Dénès
2017-07-21Adding a V8.7 compatibility version number.Hugo Herbelin
2017-07-16Removing a dummy parameter in some FMapPositive statements.Hugo Herbelin
2017-07-05Fix typo in documentation for identityTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-29Fix Zmod_div.Russell O'Connor
2017-06-29Use forall for consistencyroconnor-blockstream
2017-06-29Add Z.mod_div lemma to standard library.Russell O'Connor
2017-06-26Merge PR#826: Put plugin exports in the right compatibility fileMaxime Dénès
2017-06-23Merge PR#794: Cleanup of ltac cmxsMaxime Dénès
2017-06-22Put plugin exports in the right compatibility fileJason Gross
2017-06-15plugins/ltac : avoid spurious .cmxs filesPierre Letouzey
2017-06-15Merge PR#375: DeprecationMaxime Dénès
2017-06-14Merge PR#753: Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Maxime Dénès
2017-06-14Prelude : no more autoload of plugins extraction and recdefPierre Letouzey
2017-06-14Remove deprecated options from the standard library.Guillaume Melquiond
2017-06-14Remove support for Coq 8.4.Guillaume Melquiond
2017-06-14Merge PR#498: Bignums as a separate opam packageMaxime Dénès
2017-06-13Merge PR#385: Equality of sigma typesMaxime Dénès
2017-06-13BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo)Pierre Letouzey
2017-06-10Remove remaining vo.itarget files (obsolete since PR #499)Pierre Letouzey
2017-06-08Fix bug 5026 (the stdlib shouldn't define inconsistent notations).Théo Zimmermann
2017-06-01drop vo.itarget files and compute the corresponding the corresponding values ...Matej Kosik
2017-05-28More uniform indentation of sigma lemmasJason Gross
2017-05-28Give explicit proof terms to proj2_sig_eq etc.Jason Gross
2017-05-28Use the rew dependent notation in ex, ex2 proofsJason Gross
2017-05-28Make theorems about ex equality QedJason Gross
2017-05-28Make new proofs of equality QedJason Gross
2017-05-28Add some more comments about sigma equalitiesJason Gross
2017-05-28Remove motive argument from [rew dependent]Jason Gross
2017-05-28Use a local [rew dependent] notationJason Gross
2017-05-28Add forward-chaining versions: [eq_sig*_uncurried]Jason Gross
2017-05-28Use notation for sigTJason Gross
2017-05-28Remove reference to [IsIso]Jason Gross
2017-05-28Use notations for [sig], [sigT], [sig2], [sigT2]Jason Gross
2017-05-28Use extended notation for ex, ex2 typesJason Gross
2017-05-28Replace [ex'] with [ex]Jason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
2017-05-28Add equality lemmas for sig2 and sigT2Jason Gross
2017-05-28Add lemmas for ex2Jason Gross
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add an [inversion_sigma] tacticJason Gross
2017-05-28Add lemmas about equality of sigma typesJason Gross
2017-05-28Use [rew_] instead of [eq_rect_] prefixJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 13:03:58 +0000