Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | Merge branch 'v8.6' into trunk | 2017-03-23 | ||
|\ \ \ \ \ \ \ | | |_|_|/ / / | |/| | | | | | ||||
* | | | | | | | Make IZR a morphism for field. | 2017-03-22 | ||
* | | | | | | | Change the parser and printer so that they use IZR for real constants. | 2017-03-22 | ||
* | | | | | | | Make IZR use a compact representation of integers. | 2017-03-22 | ||
* | | | | | | | Simplify some proofs using ring and field. | 2017-03-22 | ||
* | | | | | | | Add a forgotten (?) line to "theories/Logic/vo.itarget". | 2017-03-19 | ||
* | | | | | | | Merge PR#442: Allow interactive editing of Coq.Init.Logic | 2017-03-17 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR#451: Add η principles for sigma types | 2017-03-17 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto | 2017-03-14 | ||
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / |/| | | | | | | | | ||||
| | | | * | | | | | Fix 3 unused-intro-pattern warnings in stdlib. | 2017-03-14 | ||
* | | | | | | | | | Merge PR#318: Providing a file in the Logic library to work with extensional ... | 2017-03-09 | ||
|\ \ \ \ \ \ \ \ \ | ||||
| | | | | | | * | | | Farewell decl_mode | 2017-03-07 | ||
| |_|_|_|_|_|/ / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR#279: A few lemmas about iff and about orders on positive and Z | 2017-03-06 | ||
|\ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | Strengthening some of the results in ChoiceFacts.v. | 2017-03-03 | ||
| | * | | | | | | | | Adding explicitly a file to work in the context of propositional extensionality. | 2017-03-03 | ||
| | * | | | | | | | | Adding a file providing extensional choice (i.e. choice over setoids). | 2017-03-03 | ||
| | * | | | | | | | | Adding various properties and characterization of the extensional | 2017-03-03 | ||
| | * | | | | | | | | Slightly unifying renaming in ChoiceFacts.v. | 2017-03-03 | ||
| | * | | | | | | | | Logic library: Adding a characterization of excluded-middle in term of | 2017-03-03 | ||
* | | | | | | | | | | Merge PR#273: Tidy stdlib | 2017-03-03 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
| | * | | | | | | | | | Completing basic lemmas about <= and < in BinInt.Z.Pos2Z. | 2017-03-03 | ||
| | * | | | | | | | | | Relying on BinInt.Z.Pos2Z for proofs of a few lemmas in Zorder. | 2017-03-03 | ||
| | * | | | | | | | | | Completing "few lemmas about Zneg" with lemmas also about Zpos. | 2017-03-03 | ||
| | * | | | | | | | | | A couple of other useful properties about compare_cont. | 2017-03-03 | ||
| | * | | | | | | | | | Compatibility of iff wrt not and imp. | 2017-03-03 | ||
| |/ / / / / / / / / |/| | | | | | | | | | ||||
| | * | | | | | | | | Formatting references with surrounding brackets in Diaconescu.v. | 2017-03-03 | ||
| |/ / / / / / / / |/| | | | | | | | | ||||
| | | * | | | | | | Add η principles for sigma types | 2017-03-01 | ||
| | | * | | | | | | Remove some trailing whitespace in Init/Specif.v | 2017-03-01 | ||
| |_|/ / / / / / |/| | | | | | | | ||||
| | * | | | | | | Simplifying the proof of NoRetractToModalProposition.paradox in | 2017-02-24 | ||
| |/ / / / / / |/| | | | | | | ||||
| | | | | * | | Fixing a little bug in printing ex2 (type was printed "_" by default). | 2017-02-23 | ||
| | * | | | | | Allow interactive editing of Coq.Init.Logic | 2017-02-21 | ||
| |/ / / / / |/| | | | | | ||||
* | | | | | | Ltac as a plugin. | 2017-02-17 | ||
| | | | | * | Added some theory on powerRZ. | 2017-02-15 | ||
| |_|_|_|/ |/| | | | | ||||
| * | | | | Proof clean-up. | 2017-01-30 | ||
|/ / / / | ||||
| | | * | Fix some documentation typos. | 2016-12-26 | ||
* | | | | Fix a typo in Hurkens.v comment | 2016-12-19 | ||
| | * | | strengthened the statement of JMeq_eq_dep | 2016-12-11 | ||
| |/ / |/| | | ||||
* | | | Merge branch 'v8.6' | 2016-11-30 | ||
|\| | | ||||
| * | | Fix some documentation typos. | 2016-11-24 | ||
| * | | Fix some documentation typos. | 2016-11-24 | ||
* | | | Merge branch 'v8.6' | 2016-11-18 | ||
|\| | | ||||
| * | | Merge commit 'e6edb33' into v8.6 | 2016-11-07 | ||
| |\ \ | ||||
| | * | | More explicit name for status of unification constraints. | 2016-11-07 | ||
| * | | | Merge remote-tracking branch 'github/pr/336' into v8.6 | 2016-11-04 | ||
| |\ \ \ | ||||
| * | | | | Silence option deprecation warnings in the compat file | 2016-11-04 | ||
| | * | | | Remove v62 from stdlib. | 2016-10-24 | ||
| |/ / / | ||||
| | * / | Add Unset Use Unif Heuristics in Compat/Coq85 | 2016-10-22 | ||
| |/ / | ||||
* | | | Merge branch 'v8.6' | 2016-10-17 | ||
|\| | | ||||
| * | | Fix previous commit. | 2016-10-17 | ||
| * | | Merge PR #300 into v8.6 | 2016-10-17 | ||
| |\ \ |