aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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
2017-04-28Allow interactive editing of {C,}Morphisms in PGJason Gross
2017-04-28Add .dir-locals.el and _CoqProject files for emacs stdlib editingJason Gross
2017-04-27Merge PR#414: Some more theory on powerRZ.Maxime Dénès
2017-04-27Merge PR#584: Give andb_prop a simpler proofMaxime Dénès
2017-04-26Small typo in commentVadim Zaliva
2017-04-25Add transparent_abstract tacticJason Gross
2017-04-25Give andb_prop a simpler proofJason Gross
2017-04-19Merge PR#545: Add some hints to the "real" database to automatically discharg...Maxime Dénès
2017-04-15Merge branch 'v8.6' into trunkMaxime Dénès
2017-04-07Add some hints to the "real" database to automatically discharge literal comp...Guillaume Melquiond
2017-04-06Merge PR#455: Farewell decl_modeMaxime Dénès
2017-04-06Merge branch 'origin/v8.5' into v8.6.Hugo Herbelin
2017-04-02Fix documentation typo (bug #5433).Guillaume Melquiond
2017-04-02Simplify some proofs.Guillaume Melquiond
2017-03-30Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Guillaume Melquiond
2017-03-30Merge PR#469: Added take to VectorDefMaxime Dénès
2017-03-30Added take to VectorDef.George Stelle
2017-03-28Fixing missing PropFacts.v in Logic/vo.itarget.Hugo Herbelin
2017-03-24Merge PR#392: strengthened the statement of JMeq_eq_depMaxime Dénès
2017-03-23Merge branch 'v8.6' into trunkMaxime Dénès
2017-03-22Make IZR a morphism for field.Guillaume Melquiond
2017-03-22Change the parser and printer so that they use IZR for real constants.Guillaume Melquiond
2017-03-22Make IZR use a compact representation of integers.Guillaume Melquiond
2017-03-22Simplify some proofs using ring and field.Guillaume Melquiond
2017-03-19Add a forgotten (?) line to "theories/Logic/vo.itarget".Matej Kosik
2017-03-17Merge PR#442: Allow interactive editing of Coq.Init.LogicMaxime Dénès
2017-03-17Merge PR#451: Add η principles for sigma typesMaxime Dénès
2017-03-14Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoMaxime Dénès
2017-03-14Fix 3 unused-intro-pattern warnings in stdlib.Théo Zimmermann
2017-03-09Merge PR#318: Providing a file in the Logic library to work with extensional ...Maxime Dénès
2017-03-07Farewell decl_modeEnrico Tassi
2017-03-06Merge PR#279: A few lemmas about iff and about orders on positive and ZMaxime Dénès
2017-03-03Strengthening some of the results in ChoiceFacts.v.Hugo Herbelin
2017-03-03Adding explicitly a file to work in the context of propositional extensionality.Hugo Herbelin
2017-03-03Adding a file providing extensional choice (i.e. choice over setoids).Hugo Herbelin
2017-03-03Adding various properties and characterization of the extensionalHugo Herbelin
2017-03-03Slightly unifying renaming in ChoiceFacts.v.Hugo Herbelin
2017-03-03Logic library: Adding a characterization of excluded-middle in term ofHugo Herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-13 18:32:37 +0000