Commit message (Expand) | Author | Age | |
---|---|---|---|
* | Merge PR#437: Improve unification debug trace. | Maxime Dénès | 2017-03-17 |
|\ | |||
* \ | Merge PR#445: TACTIC EXTEND now takes an optional level as argument. | Maxime Dénès | 2017-03-17 |
|\ \ | |||
* \ \ | 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 |
|\ \ \ \ | |||
* | | | | | Attempt to improve error message when "apply in" fail. | Hugo Herbelin | 2017-03-15 |
* | | | | | Merge PR#267: Proposal for an update of the recommended style in programming ... | Maxime Dénès | 2017-03-15 |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR#444: Simplifying a statement in Hurkens.v + a case study for eauto | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR#438: Fix V7 syntax in refman. | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR#412: Remove outdated comment from 2002. | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR#432: [cleanup] Change Id.t option to Name.t in TacFun | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ | Merge PR#477: [travis] Basic support for overlays. | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ | Merge PR#473: [ci] Document that sudo: false is slower | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#464: [META] More fixes | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#446: Remove a dead exception catching code. | Maxime Dénès | 2017-03-14 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | | | | [travis] Basic support for overlays. | Emilio Jesus Gallego Arias | 2017-03-13 |
| |_|_|/ / / / / / / / / / |/| | | | | | | | | | | | | |||
| * | | | | | | | | | | | | Remove a dead exception catching code. | Théo Zimmermann | 2017-03-13 |
|/ / / / / / / / / / / / | |||
* | | | | | | | | | | | | Merge PR#456: Proposing improvement to the CI targets for local use | Maxime Dénès | 2017-03-13 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | | | Updating core.dbg after ltac moved to plugins directory. | Hugo Herbelin | 2017-03-12 |
| * | | | | | | | | | | | | [travis] Make the git_checkout function more reliable. | Théo Zimmermann | 2017-03-10 |
| * | | | | | | | | | | | | [travis] Adding a template file and using it for all targets. | Théo Zimmermann | 2017-03-10 |
| * | | | | | | | | | | | | [travis] Change headband for wider compatibility. | Théo Zimmermann | 2017-03-10 |
| * | | | | | | | | | | | | Improve build of travis target on local machine. | Théo Zimmermann | 2017-03-10 |
|/ / / / / / / / / / / / | |||
| | * / / / / / / / / / | [ci] Document that sudo: false is slower | Tej Chajed | 2017-03-10 |
| |/ / / / / / / / / / |/| | | | | | | | | | | |||
| * | | | | | | | | | | [META] [build] Install dlls to kernel/byterun | Emilio Jesus Gallego Arias | 2017-03-10 |
| * | | | | | | | | | | [META] Ltac now a plugin. | Emilio Jesus Gallego Arias | 2017-03-10 |
| * | | | | | | | | | | [META] Update version number. | Emilio Jesus Gallego Arias | 2017-03-10 |
* | | | | | | | | | | | Merge PR#468: [travis] Fix GeoCoq and move it to allow fail. | Maxime Dénès | 2017-03-10 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | | Typo doc notations. | Hugo Herbelin | 2017-03-09 |
* | | | | | | | | | | | | Clarifying doc about interpretation of scopes in notations (#5386). | Hugo Herbelin | 2017-03-09 |
| * | | | | | | | | | | | [travis] Move GeoCoq to allow fail. | Emilio Jesus Gallego Arias | 2017-03-09 |
| |/ / / / / / / / / / | |||
* | | | | | | | | | | | Merge PR#318: Providing a file in the Logic library to work with extensional ... | Maxime Dénès | 2017-03-09 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* | | | | | | | | | | | | Micromega: removing a constant preventing micromega to be loaded before Logic.v. | Hugo Herbelin | 2017-03-09 |
* | | | | | | | | | | | | Fixing dependency order of plugins. | Hugo Herbelin | 2017-03-09 |
| |/ / / / / / / / / / |/| | | | | | | | | | | |||
* | | | | | | | | | | | Fixing Bug 5383 (Hyps Limit) + small refactoring. | Pierre Courtieu | 2017-03-07 |
* | | | | | | | | | | | Merge PR#436: [ocamlbuild] Update META for the vernac split. | Maxime Dénès | 2017-03-07 |
|\ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR#447: [travis] [External CI] fiat-parsers | Maxime Dénès | 2017-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR#279: A few lemmas about iff and about orders on positive and Z | Maxime Dénès | 2017-03-06 |
|\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | * | | | | | | | | | | CHANGES: choice over setoids and prop. ext. | Hugo Herbelin | 2017-03-03 |
| | | | * | | | | | | | | | | 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 |