Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | Merge PR#414: Some more theory on powerRZ. | Maxime Dénès | 2017-04-27 | |
|\ \ | ||||
* \ \ | Merge PR#584: Give andb_prop a simpler proof | Maxime Dénès | 2017-04-27 | |
|\ \ \ | ||||
* | | | | Small typo in comment | Vadim Zaliva | 2017-04-26 | |
| | | * | Add transparent_abstract tactic | Jason Gross | 2017-04-25 | |
| |_|/ |/| | | ||||
| * | | Give andb_prop a simpler proof | Jason Gross | 2017-04-25 | |
|/ / | ||||
* | | Merge PR#545: Add some hints to the "real" database to automatically discharg... | Maxime Dénès | 2017-04-19 | |
|\ \ | ||||
* \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-04-15 | |
|\ \ \ | ||||
| | * | | Add some hints to the "real" database to automatically discharge literal comp... | Guillaume Melquiond | 2017-04-07 | |
| |/ / |/| | | ||||
* | | | Merge PR#455: Farewell decl_mode | Maxime Dénès | 2017-04-06 | |
|\ \ \ | ||||
| | * \ | Merge branch 'origin/v8.5' into v8.6. | Hugo Herbelin | 2017-04-06 | |
| | |\ \ | ||||
* | | | | | Fix documentation typo (bug #5433). | Guillaume Melquiond | 2017-04-02 | |
* | | | | | Simplify some proofs. | Guillaume Melquiond | 2017-04-02 | |
* | | | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R. | Guillaume Melquiond | 2017-03-30 | |
* | | | | | Merge PR#469: Added take to VectorDef | Maxime Dénès | 2017-03-30 | |
|\ \ \ \ \ | ||||
| * | | | | | Added take to VectorDef. | George Stelle | 2017-03-30 | |
* | | | | | | Fixing missing PropFacts.v in Logic/vo.itarget. | Hugo Herbelin | 2017-03-28 | |
* | | | | | | Merge PR#392: strengthened the statement of JMeq_eq_dep | Maxime Dénès | 2017-03-24 | |
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge branch 'v8.6' into trunk | Maxime Dénès | 2017-03-23 | |
|\ \ \ \ \ \ \ | | |_|_|/ / / | |/| | | | | | ||||
* | | | | | | | Make IZR a morphism for field. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | | Change the parser and printer so that they use IZR for real constants. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | | Make IZR use a compact representation of integers. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | | Simplify some proofs using ring and field. | Guillaume Melquiond | 2017-03-22 | |
* | | | | | | | Add a forgotten (?) line to "theories/Logic/vo.itarget". | Matej Kosik | 2017-03-19 | |
* | | | | | | | Merge PR#442: Allow interactive editing of Coq.Init.Logic | Maxime Dénès | 2017-03-17 | |
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR#451: Add η principles for sigma types | Maxime Dénès | 2017-03-17 | |
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto | Maxime Dénès | 2017-03-14 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| | | | * | | | | | Fix 3 unused-intro-pattern warnings in stdlib. | Théo Zimmermann | 2017-03-14 | |
* | | | | | | | | | Merge PR#318: Providing a file in the Logic library to work with extensional ... | Maxime Dénès | 2017-03-09 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | Farewell decl_mode | Enrico Tassi | 2017-03-07 | |
| |_|_|_|_|_|/ / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR#279: A few lemmas about iff and about orders on positive and Z | Maxime Dénès | 2017-03-06 | |
|\ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | Strengthening some of the results in ChoiceFacts.v. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | Adding explicitly a file to work in the context of propositional extensionality. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | Adding a file providing extensional choice (i.e. choice over setoids). | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | Adding various properties and characterization of the extensional | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | Slightly unifying renaming in ChoiceFacts.v. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | Logic library: Adding a characterization of excluded-middle in term of | Hugo Herbelin | 2017-03-03 | |
* | | | | | | | | | | Merge PR#273: Tidy stdlib | Maxime Dénès | 2017-03-03 | |
|\ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | | Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | | Completing "few lemmas about Zneg" with lemmas also about Zpos. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | | A couple of other useful properties about compare_cont. | Hugo Herbelin | 2017-03-03 | |
| | * | | | | | | | | | Compatibility of iff wrt not and imp. | Hugo Herbelin | 2017-03-03 | |
| |/ / / / / / / / / |/| | | | | | | | | | ||||
| | * | | | | | | | | Formatting references with surrounding brackets in Diaconescu.v. | Hugo Herbelin | 2017-03-03 | |
| |/ / / / / / / / |/| | | | | | | | | ||||
| | | * | | | | | | Add η principles for sigma types | Jason Gross | 2017-03-01 | |
| | | * | | | | | | Remove some trailing whitespace in Init/Specif.v | Jason Gross | 2017-03-01 | |
| |_|/ / / / / / |/| | | | | | | | ||||
| | * | | | | | | Simplifying the proof of NoRetractToModalProposition.paradox in | Hugo Herbelin | 2017-02-24 | |
| |/ / / / / / |/| | | | | | | ||||
| | | | | * | | Fixing a little bug in printing ex2 (type was printed "_" by default). | Hugo Herbelin | 2017-02-23 | |
| | * | | | | | Allow interactive editing of Coq.Init.Logic | Jason Gross | 2017-02-21 | |
| |/ / / / / |/| | | | | | ||||
* | | | | | | Ltac as a plugin. | Pierre-Marie Pédrot | 2017-02-17 | |
| | | | | * | Added some theory on powerRZ. | Thomas Sibut-Pinote | 2017-02-15 | |
| |_|_|_|/ |/| | | | |