Commit message (Expand) | Author | Age | |
---|---|---|---|
* | [located] More work towards using CAst.t | 2018-03-09 | |
* | Merge PR #6775: Allow using cumulativity without forcing strict constraints. | 2018-03-09 | |
|\ | |||
* \ | Merge PR #6769: Split closure cache and remove whd_both | 2018-03-09 | |
|\ \ | |||
| | * | Allow using cumulativity without forcing strict constraints. | 2018-03-09 | |
* | | | Implement the Export Set/Unset feature. | 2018-03-09 | |
| |/ |/| | |||
* | | Merge PR #6496: Generate typed generic code from ltac macros | 2018-03-09 | |
|\ \ | |||
* \ \ | Merge PR #6926: An experimental 'Show Extraction' command (grant feature wish... | 2018-03-08 | |
|\ \ \ | |||
* \ \ \ | Merge PR #6893: Cleanup UState API usage | 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 | |
|\ \ \ \ | |||
* \ \ \ \ | Merge PR #6909: Deprecate Focus and Unfocus | 2018-03-08 | |
|\ \ \ \ \ | |||
* \ \ \ \ \ | Merge PR #6934: Warn when using “Require” in a section | 2018-03-08 | |
|\ \ \ \ \ \ | |||
* \ \ \ \ \ \ | Merge PR #6783: ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | 2018-03-08 | |
|\ \ \ \ \ \ \ | |||
| | * | | | | | | [stdlib] Do not use “Require” inside sections | 2018-03-07 | |
| |/ / / / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6932: [stdlib] Do not use deprecated notations | 2018-03-07 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6905: Fix make ml-doc | 2018-03-07 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6911: [ssr] Declare prenex implicits for `Some_inj` | 2018-03-07 | |
|\ \ \ \ \ \ \ \ \ | |||
| | | | | | | | * | | An experimental 'Show Extraction' command (grant feature wish #4129) | 2018-03-06 | |
| | | | | | | | * | | Extraction: switch to EConstr.t as the central type to extract from. | 2018-03-06 | |
| | | | | | * | | | | romega: get rid of EConstr.Unsafe | 2018-03-06 | |
| | | | | | | |/ / | | | | | | |/| | | |||
| | | * | | / | | | [stdlib] Do not use deprecated notations | 2018-03-06 | |
| |_|/ / / / / / |/| | | | | | | | |||
| | | | | | * | | Rename some universe minimizing "normalize" functions to "minimize" | 2018-03-06 | |
| | | | | | * | | Deprecate UState aliases in Evd. | 2018-03-06 | |
| |_|_|_|_|/ / |/| | | | | | | |||
* | | | | | | | Merge PR #6795: [ssreflect] Export parsing witnesses in mli file. | 2018-03-06 | |
|\ \ \ \ \ \ \ | |||
| | | | * | | | | ssr: use `apply_type ~typecheck:true` everywhere (fix #6634) | 2018-03-06 | |
* | | | | | | | | Merge PR #6896: [compat] Remove NOOP deprecated options. | 2018-03-06 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6898: [compat] Remove "Intuition Iff Unfolding" | 2018-03-06 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|/ / / / |/| | | | | | | | | |||
| | | | | * | | | | Escape curly braces in ocamldoc comment | 2018-03-05 | |
| | | | | * | | | | Separate vim/emacs fold markers from ocamldoc comments | 2018-03-05 | |
| |_|_|_|/ / / / |/| | | | | | | | |||
| | | * | | | | | [ssreflect] Export parsing witnesses in mli file. | 2018-03-05 | |
| |_|/ / / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6855: Update headers following #6543. | 2018-03-05 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6700: [ssr] rewrite Ssripats and Ssrview in the tactic monad | 2018-03-05 | |
|\ \ \ \ \ \ \ \ | |||
| | | | * | | | | | [compat] Remove NOOP and alias deprecated options. | 2018-03-04 | |
| |_|_|/ / / / / |/| | | | | | | | |||
| | | | * | | | | ssr: add Prenex Implicits for Some_inj to use it as a view | 2018-03-04 | |
| | | | * | | | | ssr: fix typo in doc comment | 2018-03-04 | |
| |_|_|/ / / / |/| | | | | | | |||
| * | | | | | | ssr: ipats: V82.tactic ~nf_evars:false everywhere | 2018-03-04 | |
| * | | | | | | ssr: rewrite Ssripats and Ssrview in the tactic monad | 2018-03-04 | |
* | | | | | | | Merge PR #6791: Removing compatibility support for versions older than 8.5. | 2018-03-04 | |
|\ \ \ \ \ \ \ | |/ / / / / / |/| | | | | | | |||
* | | | | | | | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | 2018-03-04 | |
|\ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ | Merge PR #6846: Moving code for "simple induction"/"simple destruct" to coret... | 2018-03-04 | |
|\ \ \ \ \ \ \ \ | |||
* \ \ \ \ \ \ \ \ | Merge PR #6676: [proofview] goals come with a state | 2018-03-04 | |
|\ \ \ \ \ \ \ \ \ | |_|_|_|_|_|_|/ / |/| | | | | | | | | |||
| | | | | | | | * | Pass the constant cache as a separate argument in kernel reduction. | 2018-03-04 | |
| |_|_|_|_|_|_|/ |/| | | | | | | | |||
| | | | | | | * | Remove all uses of Focus in standard library. | 2018-03-04 | |
| |_|_|_|_|_|/ |/| | | | | | | |||
| | | | | | * | [compat] Remove "Intuition Iff Unfolding" | 2018-03-03 | |
| |_|_|_|_|/ |/| | | | | | |||
| | | | * | | Turn warning for deprecated notations on. | 2018-03-02 | |
| |_|_|/ / |/| | | | | |||
| | * | | | Moving code for "simple induction"/"simple destruct" to coretactics.ml4. | 2018-03-01 | |
| |/ / / |/| | | | |||
| | * | | [econstr] Continue consolidation of EConstr API under `interp`. | 2018-02-28 | |
| |/ / |/| | | |||
* | | | Merge PR #6788: Fixes #6787 (minus sign interpreted by coqdoc as a bullet in ... | 2018-02-28 | |
|\ \ \ | |||
| | | * | Update headers following #6543. | 2018-02-27 | |
| |_|/ |/| | | |||
* | | | [ast] Improve precision of Ast location recognition in serialization. | 2018-02-22 |