| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2018-03-04 | ssr: fix typo in doc comment | Anton Trunov | |
| 2018-03-04 | Merge PR #935: Handling evars in the VM | Maxime Dénès | |
| 2018-03-04 | ssr: ipats: V82.tactic ~nf_evars:false everywhere | Enrico Tassi | |
| 2018-03-04 | Proofview: V82.tactic option to not normalize evars | Enrico Tassi | |
| 2018-03-04 | ssr: rewrite Ssripats and Ssrview in the tactic monad | Enrico Tassi | |
| Ssripats and Ssrview are now written in the Tactic Monad. Ssripats implements the => tactical. Ssrview implements the application of forward views. The code is, according to my tests, 100% backward compatible. The code is much more documented than before. Moreover the "ist" (ltac context) used to interpret views is the correct one (the one at ARGUMENT EXTEND interp time, not the one at TACTIC EXTEND execution time). Some of the code not touched by this commit still uses the incorrect ist, so its visibility in TACTIC EXTEND can't be removed yet. The main changes in the code are: - intro patterns are implemented using a state machine (a goal comes with a state). Ssrcommon.MakeState provides an easy way for a tactic to enrich the goal with with data of interest, such as the set of hyps to be cleared. This cleans up the old implementation that, in order to thread the state, that to redefine a bunch of tclSTUFF - the interpretation of (multiple) forward views uses the state to accumulate intermediate results - the bottom of Sscommon collects a bunch of utilities written in the tactic monad. Most of them are the rewriting of already existing utilities. When possible the old version was removed. | |||
| 2018-03-04 | tactics: export e_reduct_in_concl | Enrico Tassi | |
| 2018-03-04 | reductionops: remove dead code "bind_assum" | Enrico Tassi | |
| 2018-03-04 | proofview: debug API to print a goal | Enrico Tassi | |
| 2018-03-04 | Merge PR #6791: Removing compatibility support for versions older than 8.5. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6736: [toplevel] Move beautify to its own pass. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6876: Unify Const_sorts and Const_type, and remove Vsort | Maxime Dénès | |
| 2018-03-04 | Merge PR #6846: Moving code for "simple induction"/"simple destruct" to ↵ | Maxime Dénès | |
| coretactics.ml4. | |||
| 2018-03-04 | Merge PR #6885: [stm] Partial fix for bug #6884 [location missing from ↵ | Maxime Dénès | |
| replay nodes] | |||
| 2018-03-04 | Merge PR #6873: [toplevel] Update state when `Drop` exception is thrown [#6872] | Maxime Dénès | |
| 2018-03-04 | Merge PR #6882: Harden gitattributes against core.whitespace configuration. | Maxime Dénès | |
| 2018-03-04 | Merge PR #6879: Fix #6878: univ undefined for [with Definition] bad instance ↵ | Maxime Dénès | |
| size. | |||
| 2018-03-04 | Merge PR #6676: [proofview] goals come with a state | Maxime Dénès | |
| 2018-03-04 | Merge PR #915: Fix rewrite in * side conditions | Maxime Dénès | |
| 2018-03-04 | Merge PR #6735: [toplevel] [vernac] Remove Load hack and check / document ↵ | Maxime Dénès | |
| supported scenarios. | |||
| 2018-03-04 | Remove whd_both from the kernel. | Pierre-Marie Pédrot | |
| Now that the cache is distinct, there should be no nasty side-effects changing the value of one side while reducing the other. | |||
| 2018-03-04 | Pass the constant cache as a separate argument in kernel reduction. | Pierre-Marie Pédrot | |
| 2018-03-04 | Remove all uses of Focus in standard library. | Théo Zimmermann | |
| 2018-03-04 | Fix typos. | Théo Zimmermann | |
| 2018-03-03 | Removing test for bug #2850. | Pierre-Marie Pédrot | |
| This test was actually checking that evar-containing terms were making the VM fail. Obviously this is not the case anymore, so the test is now invalid. | |||
| 2018-03-03 | Adding a test file for evar handling in the VM. | Pierre-Marie Pédrot | |
| 2018-03-03 | Handling evars in the VM. | Pierre-Marie Pédrot | |
| We simply treat them as as an application of an atom to its instance, and in the decompilation phase we reconstruct the instance from the stack. This grants wish BZ#5659. | |||
| 2018-03-03 | [compat] Remove "Tactic Pattern Unification" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Tactic Pattern Unification" | |||
| 2018-03-03 | [compat] Remove "Standard Proposition Elimination" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Standard Proposition Elimination" | |||
| 2018-03-03 | [compat] Remove "Intuition Iff Unfolding" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Intuition Iff Unfolding" | |||
| 2018-03-03 | [compat] Remove "Injection L2R Pattern Order" | Emilio Jesus Gallego Arias | |
| Following up on #6791, we remove the option "Injection L2R Pattern Order". | |||
| 2018-03-02 | CHANGES entry for #6791. | Théo Zimmermann | |
| 2018-03-02 | Remove 8.5 compatibility support. | Théo Zimmermann | |
| 2018-03-02 | Remove VOld compatibility flag. | Théo Zimmermann | |
| 2018-03-02 | Turn warning for deprecated notations on. | Théo Zimmermann | |
| Fix new deprecation warnings in the standard library. | |||
| 2018-03-02 | Remove the deprecation for some 8.2-8.5 compatibility aliases. | Théo Zimmermann | |
| This was decided during the Fall WG (2017). The aliases that are kept as deprecated are the ones where the difference is only a prefix becoming a qualified module name. The intention is to turn the warning for deprecated notations on. We change the compat version to 8.6 to allow the removal of VOld and V8_5. | |||
| 2018-03-02 | [VM] Unify Const_sorts and Const_type, and remove Vsort. | Maxime Dénès | |
| This simplifies the representation of values, and brings it closer to the ones of the native compiler. | |||
| 2018-03-02 | installer: win: put addons in a separate package | Enrico Tassi | |
| 2018-03-02 | build: win: detect 404 as HTML files | Enrico Tassi | |
| 2018-03-02 | build: win: addon bignums | Enrico Tassi | |
| 2018-03-02 | build: win: support for addons | Enrico Tassi | |
| 2018-03-02 | [stm] Partial fix for bug #6884 [location missing from replay nodes] | Emilio Jesus Gallego Arias | |
| Example not yet fixed by this patch: ``` Definition u : Type. Definition m : Type. exact nat. Defined. exact bool. Defined. ``` | |||
| 2018-03-01 | Harden gitattributes against core.whitespace configuration. | Gaëtan Gilbert | |
| 2018-03-01 | Fix #6878: univ undefined for [with Definition] bad instance size. | Gaëtan Gilbert | |
| 2018-03-01 | Add source (project file / command line) to project fields. | Gaëtan Gilbert | |
| 2018-03-01 | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-". | Hugo Herbelin | |
| Noticed by Sigurd Schneider. | |||
| 2018-03-01 | Moving code for "simple induction"/"simple destruct" to coretactics.ml4. | Hugo Herbelin | |
| 2018-03-01 | Merge PR #6856: travis: elpi needs findlib >= 1.5 | Maxime Dénès | |
| 2018-03-01 | Merge PR #6864: Remove empty, wrongly located, doc file. | Maxime Dénès | |
| 2018-03-01 | Merge PR #6861: Typo in the documentation of the `pattern` tactic | Maxime Dénès | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |