Commit message (Expand) | Author | Age | ||
---|---|---|---|---|
... | ||||
| | | | | * | | doc and changes for coercion from prop/type | 2018-03-09 | ||
| | | | | * | | added test for coercion from type | 2018-03-09 | ||
| | | | | * | | allow Prop as source for coercions | 2018-03-09 | ||
| |_|_|_|/ / |/| | | | | | ||||
* | | | | | | Merge PR #6941: [toplevel] Respect COQ_COLORS environment variable | 2018-03-09 | ||
|\ \ \ \ \ \ | ||||
* \ \ \ \ \ \ | Merge PR #6945: Fix error with univ binders on monomorphic records. | 2018-03-09 | ||
|\ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ | Merge PR #6871: [build] Simpler byte/opt toplevel build. | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ | Merge PR #6155: Get rid of ' notation for Zpos in QArith | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|/ / / |/| | | | | | | | | ||||
* | | | | | | | | | Merge PR #6800: [checker] Printer cleanup. | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ | Merge PR #6747: Relax conversion of constructors according to the pCuIC model | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ | Merge PR #6328: Fix #6313: lost goals in nested ltac in refine | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ | Merge PR #407: Fix SR breakage due to allowing fixpoints on non-rec values | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6496: Generate typed generic code from ltac macros | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6937: Add empty compat file for Coq 8.8 | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6851: Fix #6830: coqdep VDFILE uses too many arguments for fiat-cry... | 2018-03-09 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | * | | | | | | | | | | | More examples about shelve/given_up in tactic-in-terms. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Cosmetic: add an expected newline in proof_global. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | A comment in Proofview.with_shelf. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Add an invariant on future goals in Proof.run_tactic. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Add an invariant on given up goals in class_tactics. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Proof engine: support for nesting tactic-in-term within other tactics. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Adding tclPUTGIVENUP/tclPUTSHELF in Proofview.Unsafe. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Add function bind in option.ml. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Proof engine: using save_future_goal when relevant. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Proof engine: adding a function to save future goals including principal one. | 2018-03-08 | ||
| | | | | * | | | | | | | | | | | Proof engine: consider the pair principal and future goals as an entity. | 2018-03-08 | ||
| |_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | Merge PR #6522: Fix core hint database issue #6521 | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6816: Adding mention of shelved/given-up status in Show Existentials | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6928: gitlab: install num for all 4.06 jobs | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish... | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6893: Cleanup UState API usage | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | | [compat] Remove "Refolding Reduction" option. | 2018-03-08 | ||
| |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / |/| | | | | | | | | | | | | | | | | | | ||||
| | | | | | | | * | | | | | | | | | | | Make most of TACTIC EXTEND macros runtime calls. | 2018-03-08 | ||
| |_|_|_|_|_|_|/ / / / / / / / / / / |/| | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | Merge PR #6918: romega: get rid of EConstr.Unsafe | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | | | | | | | | * | | coqide: queries from the query window are routed there (fix #5684) | 2018-03-08 | ||
| | | | | | | | | | | | | | * | | | | | Fix error with univ binders on monomorphic records. | 2018-03-08 | ||
* | | | | | | | | | | | | | | | | | | | Merge PR #6817: [configure]: support for profiles | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
| | | | | | | | | | * | | | | | | | | | | Fix SR breakage due to allowing fixpoints on non-rec values | 2018-03-08 | ||
| | | | | | | | | | | * | | | | | | | | | Add test-suite file for cumulative constructors | 2018-03-08 | ||
| | | | | | | | | | | * | | | | | | | | | Leave cumul constructor universes as is during unif | 2018-03-08 | ||
| | | | | | | | | | | * | | | | | | | | | Update checker to reflect rule on constructors of polymorphic inductive types | 2018-03-08 | ||
| | | | | | | | | | | * | | | | | | | | | Relax conversion of constructors according to the pCuIC model | 2018-03-08 | ||
| | | | | | | | | | | | |_|_|/ / / / / | | | | | | | | | | | |/| | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | Merge PR #6743: Add notation {x & P} for sigT | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6927: Add some missing flushes in configure. | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6899: [compat] Remove "Standard Proposition Elimination" | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6881: [windows] support -addon in build script | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / / / / / / / |/| | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6582: Mangle auto-generated names | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6933: Standard headers for C and Python. | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | ||||
* \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | Merge PR #6934: Warn when using “Require” in a section | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|_|/ / |/| | | | | | | | | | | | | | | | | | | | | | | | | ||||
* | | | | | | | | | | | | | | | | | | | | | | | | | Merge PR #6924: Clean-up remove always false useeager argument. | 2018-03-08 | ||
|\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ |