aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
2017-07-05Fix typo in documentation for identityTej Chajed
2017-07-04Bump year in headers.Pierre-Marie Pédrot
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
2017-05-28Use [rew] notations rather than [eq_rect]Jason Gross
2017-05-28Add more groupoid-like theorems about [eq]Jason Gross
2017-05-16Stop using auto with * in two proofs.Théo Zimmermann
2017-05-11Merge PR#201: Transparent abstractMaxime Dénès
2017-05-05Merge PR#605: Report a useful error for dependent inductionMaxime Dénès
2017-05-05Merge PR#593: Functional choice <-> [inhabited] and [forall] commuteMaxime Dénès
2017-05-03Merge PR#588: Allow interactive editing of {C,}Morphisms in PGMaxime Dénès
2017-05-03Merge PR#386: Better editing of the standard library in coqtop/PGMaxime Dénès
2017-05-03Report a useful error for dependent inductionTej Chajed
2017-05-03Reorganize comment documentation of ChoiceFacts.vGaetan Gilbert
2017-04-30Functional choice <-> [inhabited] and [forall] commuteGaetan Gilbert
2017-04-29Suppress warning message in stdlib.Guillaume Melquiond
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:45:22 +0000