| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2017-11-23 | Make one more function robust in term_dnet.ml | Maxime Dénès | |
| Was actually forgotten in native-coq. | |||
| 2017-11-23 | Make some functions on terms more robust w.r.t new term constructs. | Maxime Dénès | |
| Extending terms is notoriously difficult. We try to get more help from the compiler by making sure such an extension will trigger non exhaustive pattern matching warnings. | |||
| 2017-11-22 | [api] Deprecate Term destructors, move to Constr | Emilio Jesus Gallego Arias | |
| We mirror the structure of EConstr and move the destructors from `Term` to `Constr`. This is a step towards having a single module for `Constr`. | |||
| 2017-11-21 | [printing] Deprecate all printing functions accessing the global proof. | Emilio Jesus Gallego Arias | |
| We'd like to handle proofs functionally we thus recommend not to use printing functions without an explicit context. We also adapt most of the code, making more explicit where the printing environment is coming from. An open task is to refactor some code so we gradually make the `Pfedit.get_current_context ()` disappear. | |||
| 2017-11-19 | [proof] Attempt to deprecate some V82 parts of the proof API. | Emilio Jesus Gallego Arias | |
| I followed what seems to be the intention of the code, with the original intention of remove the global imperative proof state. However, I fully fail to see why the new API is better than the old one. In fact the opposite seems the contrary. Still big parts of the "new proof engine" seem unfinished, and I'm afraid I am not the right person to know what direction things should take. | |||
| 2017-11-13 | [api] Insert miscellaneous API deprecation back to core. | Emilio Jesus Gallego Arias | |
| 2017-11-13 | [api] Another large deprecation, `Nameops` | Emilio Jesus Gallego Arias | |
| 2017-11-06 | [api] Move structures deprecated in the API to the core. | Emilio Jesus Gallego Arias | |
| We do up to `Term` which is the main bulk of the changes. | |||
| 2017-11-06 | [api] Deprecate all legacy uses of Names in core. | Emilio Jesus Gallego Arias | |
| This will allow to merge back `Names` with `API.Names` | |||
| 2017-11-04 | [api] Deprecate all legacy uses of Name.Id in core. | Emilio Jesus Gallego Arias | |
| This is a first step towards some of the solutions proposed in #6008. | |||
| 2017-11-02 | Update tactics.ml | Farzon Lotfi | |
| fix spelling mistake. reword message to be in the Present Perfect tense instead of the 3rd person present because action is completed with respect to the theorem not some unknown third person. | |||
| 2017-10-27 | Merge PR #6015: [general] Remove Econstr dependency from `intf` | Maxime Dénès | |
| 2017-10-26 | Passing around the flag for injection so that tactics calling inj at | Hugo Herbelin | |
| ML level can set the flags themselves. In particular, using injection and discriminate with option "Keep Proofs Equalities" when called from "decide equality" and "Scheme Equality". This fixes bug #5281. | |||
| 2017-10-26 | Delay use of flag "Discriminate Introduction" from interp to execution time. | Hugo Herbelin | |
| 2017-10-25 | [general] Remove Econstr dependency from `intf` | Emilio Jesus Gallego Arias | |
| To this extent we factor out the relevant bits to a new file, ltac_pretype. | |||
| 2017-10-19 | Moving bug numbers to BZ# format in the source code. | Théo Zimmermann | |
| Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers. | |||
| 2017-10-09 | Merge PR #1109: Handle some misc todos | Maxime Dénès | |
| 2017-10-04 | Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial). | Maxime Dénès | |
| 2017-09-29 | Remove a failwith "" | Gaëtan Gilbert | |
| 2017-09-28 | Efficient computation of the names contained in an environment. | Pierre-Marie Pédrot | |
| 2017-09-28 | Efficient fresh name generation relying on sets. | Pierre-Marie Pédrot | |
| The old algorithm was relying on list membership, which is O(n). This was nefarious for terms with many binders. We use instead sets in O(log n). | |||
| 2017-09-26 | Merge PR #688: Binding universe constraints in Definition/Inductive/etc... | Maxime Dénès | |
| 2017-09-25 | Merge PR #1060: An optimization of tactic constructor | Maxime Dénès | |
| 2017-09-21 | Mark "Set Tactic Compat Context" as deprecated. | Guillaume Melquiond | |
| It was introduced in 8.5 for compatibility with a 8.4 bug. | |||
| 2017-09-19 | An optimization of tactic constructor. | Hugo Herbelin | |
| As was questioned on Stack Overflow and discussed on Gitter, reduction of the conclusion of the goal was done up to n+1 times for a failing call to "constructor" on an inductive type of n constructors. We do it at most once. Reworking the layout of the code at the same time. | |||
| 2017-09-19 | Fixing bug #5741 (anomaly in info_trivial). | Hugo Herbelin | |
| The bug was introduced in 1559f73. | |||
| 2017-09-19 | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666). | Maxime Dénès | |
| 2017-09-19 | Don't lose names in UState.universe_context. | Gaëtan Gilbert | |
| We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it. | |||
| 2017-09-15 | Merge PR #1046: Better error messages, fix for BZ#5723 | Maxime Dénès | |
| 2017-09-15 | Merge PR #1037: Parse directly to Sorts.family when appropriate. | Maxime Dénès | |
| 2017-09-15 | Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵ | Maxime Dénès | |
| Inductive-keyworded record failing even on non-dependent goal) | |||
| 2017-09-14 | Avoid extra failure in the "constructor" tactic (bug #5666). | Guillaume Melquiond | |
| This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n. | |||
| 2017-09-11 | Better error messages, fix for BZ#5723 | Paul Steckler | |
| 2017-09-08 | Parse directly to Sorts.family when appropriate. | Gaëtan Gilbert | |
| When we used to parse to a glob_sort but always give an empty list in the GType case we can now parse directly to Sorts.family. | |||
| 2017-09-04 | Making detyping potentially lazy. | Pierre-Marie Pédrot | |
| The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. | |||
| 2017-08-30 | Fixing part of #5707 (allowing destruct to use non dependent case analysis). | Hugo Herbelin | |
| The fix covers the case of a non-dependent goal with unavailable dependent case analysis: destruct was not seeing that it could still use non-dependent case analysis. | |||
| 2017-08-29 | Fix BZ#5697: Congruence does not work with primitive projections. | Pierre-Marie Pédrot | |
| The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records. | |||
| 2017-08-29 | Merge PR #830: Moving assert (the "Cut" rule) to new proof engine | Maxime Dénès | |
| 2017-08-29 | Merge PR #805: Functional tactics | Maxime Dénès | |
| 2017-08-01 | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas). | Maxime Dénès | |
| 2017-08-01 | Merge PR #919: Remove a few useless evar-normalizations in printing code. | Maxime Dénès | |
| 2017-07-31 | Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t instead | Maxime Dénès | |
| 2017-07-31 | better `try with` scope in `discr_positions` | amblaf | |
| 2017-07-31 | Correcting [build_discriminator] to make the test-suite pass | amblaf | |
| 2017-07-31 | Replacing tclENV with the goal environment | amblaf | |
| In functions match_eqdec and check_unused_names | |||
| 2017-07-31 | env, sigma as first arguments of functions | amblaf | |
| 2017-07-31 | Remove references to Global.env in tactics/*.ml | amblaf | |
| Only in ml files that are not related to Coq commands | |||
| 2017-07-28 | Merge PR #888: Stronger kernel types | Maxime Dénès | |
| 2017-07-27 | Fixing bug #5671 (specialize unclean wrt Metas). | Hugo Herbelin | |
| 2017-07-27 | deprecate Pp.std_ppcmds type alias | Matej Košík | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |