aboutsummaryrefslogtreecommitdiff
path: root/theories
AgeCommit message (Expand)Author
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-09Merge PR#318: Providing a file in the Logic library to work with extensional ...Maxime Dénès
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
2017-03-03Merge PR#273: Tidy stdlibMaxime Dénès
2017-03-03Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Hugo Herbelin
2017-03-03Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Hugo Herbelin
2017-03-03Completing "few lemmas about Zneg" with lemmas also about Zpos.Hugo Herbelin
2017-03-03A couple of other useful properties about compare_cont.Hugo Herbelin
2017-03-03Compatibility of iff wrt not and imp.Hugo Herbelin
2017-03-03Formatting references with surrounding brackets in Diaconescu.v.Hugo Herbelin
2017-03-01Add η principles for sigma typesJason Gross
2017-03-01Remove some trailing whitespace in Init/Specif.vJason Gross
2017-02-24Simplifying the proof of NoRetractToModalProposition.paradox inHugo Herbelin
2017-02-21Allow interactive editing of Coq.Init.LogicJason Gross
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2017-01-30Proof clean-up.Théo Zimmermann
2016-12-19Fix a typo in Hurkens.v commentJason Gross
2016-11-30Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-24Fix some documentation typos.Guillaume Melquiond
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Merge commit 'e6edb33' into v8.6Maxime Dénès
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-11-04Silence option deprecation warnings in the compat fileJason Gross
2016-10-24Remove v62 from stdlib.Théo Zimmermann
2016-10-22Add Unset Use Unif Heuristics in Compat/Coq85Matthieu Sozeau
2016-10-17Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-17Fix previous commit.Pierre-Marie Pédrot
2016-10-17Merge PR #300 into v8.6Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Merge branch 'v8.5' into v8.6Pierre-Marie Pédrot
2016-10-12Little addition to 6eede071 for consistency of style in OrdersFacts.v.Hugo Herbelin
2016-10-08Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-06Fixing unexpected "noise" introduced in commit 24d5448c.Hugo Herbelin
2016-10-05Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-05Clean up type classes flags and update compat file.Maxime Dénès
2016-10-03Remove if_then_else. Use tryif instead.Théo Zimmermann
2016-10-02More tests for tactic "subst".Hugo Herbelin
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29Move vector/list compat notations to their relevant filesJason Gross
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 16:33:56 +0000