Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
* | | | | | | | | | | 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 | ||
| |\ \ | ||||
* | | | | Merge branch 'v8.6' | 2016-10-12 | ||
|\| | | | ||||
| * | | | Merge branch 'v8.5' into v8.6 | 2016-10-12 | ||
| |\ \ \ | | | |/ | | |/| | ||||
| * | | | Little addition to 6eede071 for consistency of style in OrdersFacts.v. | 2016-10-12 | ||
* | | | | Merge branch 'v8.6' | 2016-10-08 | ||
|\| | | | ||||
| * | | | Fixing unexpected "noise" introduced in commit 24d5448c. | 2016-10-06 | ||
* | | | | Merge branch 'v8.6' | 2016-10-05 | ||
|\| | | | ||||
| * | | | Clean up type classes flags and update compat file. | 2016-10-05 | ||
| | * | | Remove if_then_else. Use tryif instead. | 2016-10-03 | ||
| * | | | More tests for tactic "subst". | 2016-10-02 | ||
* | | | | Merge branch 'v8.6' | 2016-10-02 | ||
|\| | | | ||||
| | | * | Move vector/list compat notations to their relevant files | 2016-09-29 | ||
| | |/ | |/| | ||||
| * | | ZDivEucl: notations in different scope to avoid a warning | 2016-09-28 | ||
* | | | Merge branch 'v8.6' | 2016-09-27 | ||
|\| | | ||||
| * | | Remove spaces from around list notations | 2016-09-26 | ||
| * | | Remove spaces from around vector notations | 2016-09-26 | ||
| * | | Unbreak Ltac [ | .. | ] notation in -compat 8.5 | 2016-09-26 | ||
| * | | Fix bug #4785 (use [ ] for vector nil) | 2016-09-26 | ||
* | | | Merge branch 'v8.6' | 2016-09-23 | ||
|\| | | ||||
* | | | extensionality: Handle dependently-used hypotheses | 2016-09-19 |