aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories
Commit message (Expand)AuthorAge
* Merge PR#545: Add some hints to the "real" database to automatically discharg...Gravatar Maxime Dénès2017-04-19
|\
* \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-04-15
|\ \
| | * Add some hints to the "real" database to automatically discharge literal comp...Gravatar Guillaume Melquiond2017-04-07
| |/ |/|
* | Merge PR#455: Farewell decl_modeGravatar Maxime Dénès2017-04-06
|\ \
| | * Merge branch 'origin/v8.5' into v8.6.Gravatar Hugo Herbelin2017-04-06
| | |\
* | | | Fix documentation typo (bug #5433).Gravatar Guillaume Melquiond2017-04-02
* | | | Simplify some proofs.Gravatar Guillaume Melquiond2017-04-02
* | | | Fix ring_simplify sometimes producing R0 and R1 instead of 0%R and 1%R.Gravatar Guillaume Melquiond2017-03-30
* | | | Merge PR#469: Added take to VectorDefGravatar Maxime Dénès2017-03-30
|\ \ \ \
| * | | | Added take to VectorDef.Gravatar George Stelle2017-03-30
* | | | | Fixing missing PropFacts.v in Logic/vo.itarget.Gravatar Hugo Herbelin2017-03-28
* | | | | Merge PR#392: strengthened the statement of JMeq_eq_depGravatar Maxime Dénès2017-03-24
|\ \ \ \ \
* \ \ \ \ \ Merge branch 'v8.6' into trunkGravatar Maxime Dénès2017-03-23
|\ \ \ \ \ \ | | |_|_|/ / | |/| | | |
* | | | | | Make IZR a morphism for field.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Change the parser and printer so that they use IZR for real constants.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Make IZR use a compact representation of integers.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Simplify some proofs using ring and field.Gravatar Guillaume Melquiond2017-03-22
* | | | | | Add a forgotten (?) line to "theories/Logic/vo.itarget".Gravatar Matej Kosik2017-03-19
* | | | | | Merge PR#442: Allow interactive editing of Coq.Init.LogicGravatar Maxime Dénès2017-03-17
|\ \ \ \ \ \
* \ \ \ \ \ \ Merge PR#451: Add η principles for sigma typesGravatar Maxime Dénès2017-03-17
|\ \ \ \ \ \ \
* \ \ \ \ \ \ \ Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eautoGravatar Maxime Dénès2017-03-14
|\ \ \ \ \ \ \ \ | |_|_|_|_|/ / / |/| | | | | | |
| | | | * | | | Fix 3 unused-intro-pattern warnings in stdlib.Gravatar Théo Zimmermann2017-03-14
* | | | | | | | Merge PR#318: Providing a file in the Logic library to work with extensional ...Gravatar Maxime Dénès2017-03-09
|\ \ \ \ \ \ \ \
| | | | | | | * | Farewell decl_modeGravatar Enrico Tassi2017-03-07
| |_|_|_|_|_|/ / |/| | | | | | |
* | | | | | | | Merge PR#279: A few lemmas about iff and about orders on positive and ZGravatar Maxime Dénès2017-03-06
|\ \ \ \ \ \ \ \
| | * | | | | | | Strengthening some of the results in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | Adding explicitly a file to work in the context of propositional extensionality.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | Adding a file providing extensional choice (i.e. choice over setoids).Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | Adding various properties and characterization of the extensionalGravatar Hugo Herbelin2017-03-03
| | * | | | | | | Slightly unifying renaming in ChoiceFacts.v.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | Logic library: Adding a characterization of excluded-middle in term ofGravatar Hugo Herbelin2017-03-03
* | | | | | | | | Merge PR#273: Tidy stdlibGravatar Maxime Dénès2017-03-03
|\ \ \ \ \ \ \ \ \
| | * | | | | | | | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | | Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | | Completing "few lemmas about Zneg" with lemmas also about Zpos.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | | A couple of other useful properties about compare_cont.Gravatar Hugo Herbelin2017-03-03
| | * | | | | | | | Compatibility of iff wrt not and imp.Gravatar Hugo Herbelin2017-03-03
| |/ / / / / / / / |/| | | | | | | |
| | * | | | | | | Formatting references with surrounding brackets in Diaconescu.v.Gravatar Hugo Herbelin2017-03-03
| |/ / / / / / / |/| | | | | | |
| | | * | | | | Add η principles for sigma typesGravatar Jason Gross2017-03-01
| | | * | | | | Remove some trailing whitespace in Init/Specif.vGravatar Jason Gross2017-03-01
| |_|/ / / / / |/| | | | | |
| | * | | | | Simplifying the proof of NoRetractToModalProposition.paradox inGravatar Hugo Herbelin2017-02-24
| |/ / / / / |/| | | | |
| | | | | * Fixing a little bug in printing ex2 (type was printed "_" by default).Gravatar Hugo Herbelin2017-02-23
| | * | | | Allow interactive editing of Coq.Init.LogicGravatar Jason Gross2017-02-21
| |/ / / / |/| | | |
* | | | | Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
| * | | | Proof clean-up.Gravatar Théo Zimmermann2017-01-30
|/ / / /
| | | * Fix some documentation typos.Gravatar Guillaume Melquiond2016-12-26
* | | | Fix a typo in Hurkens.v commentGravatar Jason Gross2016-12-19
| | * | strengthened the statement of JMeq_eq_depGravatar Abhishek Anand2016-12-11
| |/ / |/| |
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-30
|\| |
| * | Fix some documentation typos.Gravatar Guillaume Melquiond2016-11-24