| Commit message (Expand) | Author | Age | |
|---|---|---|---|
| * | More examples about shelve/given_up in tactic-in-terms. |  Hugo Herbelin | 2018-03-08 |
| * | Cosmetic: add an expected newline in proof_global. | Hugo Herbelin | 2018-03-08 |
| * | A comment in Proofview.with_shelf. | Hugo Herbelin | 2018-03-08 |
| * | Add an invariant on future goals in Proof.run_tactic. | Hugo Herbelin | 2018-03-08 |
| * | Add an invariant on given up goals in class_tactics. | Hugo Herbelin | 2018-03-08 |
| * | Proof engine: support for nesting tactic-in-term within other tactics. | Hugo Herbelin | 2018-03-08 |
| * | Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe. | Hugo Herbelin | 2018-03-08 |
| * | Add function bind in option.ml. | Hugo Herbelin | 2018-03-08 |
| * | Proof engine: using save_future_goal when relevant. | Hugo Herbelin | 2018-03-08 |
| * | Proof engine: adding a function to save future goals including principal one. | Hugo Herbelin | 2018-03-08 |
| * | Proof engine: consider the pair principal and future goals as an entity. | Hugo Herbelin | 2018-03-08 |
| * | Merge PR #6522: Fix core hint database issue #6521 |  Maxime Dénès | 2018-03-08 |
| |\ | |||
| * \ | Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials | Maxime Dénès | 2018-03-08 |
| |\ \ | |||
| * \ \ | Merge PR #6928: gitlab: install num for all 4.06 jobs | Maxime Dénès | 2018-03-08 |
| |\ \ \ | |||
| * \ \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish... | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ | |||
| * \ \ \ \ | Merge PR #6893: Cleanup UState API usage | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ | |||
| * \ \ \ \ \ | Merge PR #6918: romega: get rid of EConstr.Unsafe | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ | |||
| * \ \ \ \ \ \ | Merge PR #6817: [configure]: support for profiles | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ | Merge PR #6743: Add notation {x & P} for sigT | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ | Merge PR #6927: Add some missing flushes in configure. | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ | Merge PR #6899: [compat] Remove "Standard Proposition Elimination" | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6881: [windows] support -addon in build script | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6582: Mangle auto-generated names | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6933: Standard headers for C and Python. | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6934: Warn when using “Require” in a section | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6924: Clean-up remove always false useeager argument. | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6902: [compat] Remove "Discriminate Introduction" | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6903: [compat] Remove "Shrink Abstract" | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | Maxime Dénès | 2018-03-08 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| | | | | | | | | | | | | | | | | | * | | | gitlab: install num for all jobs |  Gaëtan Gilbert | 2018-03-07 |
| | | | | | * | | | | | | | | | | | | | | | Use a proper warning when a summary is captured out of module scope. |  Vincent Laporte | 2018-03-07 |
| | | | | | * | | | | | | | | | | | | | | | [vernac] Warn when using “Require” in a section | Vincent Laporte | 2018-03-07 |
| | | | | | * | | | | | | | | | | | | | | | [stdlib] Do not use “Require” inside sections | Vincent Laporte | 2018-03-07 |
| | |_|_|_|/ / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | |||
| * | | | | | | | | | | | | | | | | | | | Merge PR #6744: Add String.concat | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6932: [stdlib] Do not use deprecated notations | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6905: Fix make ml-doc | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj` | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6922: Remove outdated information regarding the FAQ. | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6374: [toplevel] Modify printing goal strategy. | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6790: Allow universe declarations for [with Definition]. | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |||
| * \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6462: Sanitize universe declaration in Context (stop using a ref...) | Maxime Dénès | 2018-03-07 |
| |\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | | | | | | | | * | | | An experimental 'Show Extraction' command (grant feature wish #4129) |  Pierre Letouzey | 2018-03-06 |
| | | | | | | | | | | | | | | | | | | | | | | | * | | | Extraction: switch to EConstr.t as the central type to extract from. | Pierre Letouzey | 2018-03-06 |
| | | | | | | | | | | | | | | | | | | | | | * | | | | | romega: get rid of EConstr.Unsafe | Pierre Letouzey | 2018-03-06 |
| | | | | | | | | | | | | | | | | | | | | | | |/ / / | | | | | | | | | | | | | | | | | | | | | |/| | | | |||
| | | | | | | | | | | | | | | | | | | | | * | | | | | document -profile in dev/doc/setup.txt |  Enrico Tassi | 2018-03-06 |
| | | | | | | | | | | | | | * | | | | | | | | | | | | Standard headers for C and Python. | Maxime Dénès | 2018-03-06 |
| | |_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | * | | | | | | | | | | | | | | | | | [stdlib] Do not use deprecated notations | Vincent Laporte | 2018-03-06 |
| | |_|_|_|_|_|/ / / / / / / / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | | | | * | | | | | | | Add some missing flushes in configure. | Maxime Dénès | 2018-03-06 |
| | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | |||
| | | | | | | | | | | | | | * | | | | | | | | | Hack to make bignum build on windows | Enrico Tassi | 2018-03-06 |
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |