aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* [api] Deprecate Term destructors, move to ConstrGravatar Emilio Jesus Gallego Arias2017-11-22
| | | | | | | 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`.
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
| | | | | | | | | | | 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.
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
| | | | | | | | | | | | 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.
* [api] Insert miscellaneous API deprecation back to core.Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* [api] Another large deprecation, `Nameops`Gravatar Emilio Jesus Gallego Arias2017-11-13
|
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | We do up to `Term` which is the main bulk of the changes.
* [api] Deprecate all legacy uses of Names in core.Gravatar Emilio Jesus Gallego Arias2017-11-06
| | | | This will allow to merge back `Names` with `API.Names`
* [api] Deprecate all legacy uses of Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| | | | This is a first step towards some of the solutions proposed in #6008.
* Update tactics.mlGravatar Farzon Lotfi2017-11-02
| | | 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.
* Merge PR #6015: [general] Remove Econstr dependency from `intf`Gravatar Maxime Dénès2017-10-27
|\
* | Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
| | | | | | | | | | | | | | | | | | | | 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.
* | Delay use of flag "Discriminate Introduction" from interp to execution time.Gravatar Hugo Herbelin2017-10-26
| |
| * [general] Remove Econstr dependency from `intf`Gravatar Emilio Jesus Gallego Arias2017-10-25
|/ | | | | To this extent we factor out the relevant bits to a new file, ltac_pretype.
* Moving bug numbers to BZ# format in the source code.Gravatar Théo Zimmermann2017-10-19
| | | | | Compared to the original proposition (01f848d in #960), this commit only changes files containing bug numbers that are also PR numbers.
* Merge PR #1109: Handle some misc todosGravatar Maxime Dénès2017-10-09
|\
* \ Merge PR #1058: Fixing BZ#5741 (anomaly in info_trivial).Gravatar Maxime Dénès2017-10-04
|\ \
| | * Remove a failwith ""Gravatar Gaëtan Gilbert2017-09-29
| | |
* | | Efficient computation of the names contained in an environment.Gravatar Pierre-Marie Pédrot2017-09-28
| | |
* | | Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
| |/ |/| | | | | | | 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).
* | Merge PR #688: Binding universe constraints in Definition/Inductive/etc...Gravatar Maxime Dénès2017-09-26
|\ \
* \ \ Merge PR #1060: An optimization of tactic constructorGravatar Maxime Dénès2017-09-25
|\ \ \
* | | | Mark "Set Tactic Compat Context" as deprecated.Gravatar Guillaume Melquiond2017-09-21
| | | | | | | | | | | | | | | | It was introduced in 8.5 for compatibility with a 8.4 bug.
| * | | An optimization of tactic constructor.Gravatar Hugo Herbelin2017-09-19
|/ / / | | | | | | | | | | | | | | | | | | | | | | | | 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.
| | * Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
| |/ |/| | | | | The bug was introduced in 1559f73.
* | Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\ \
| | * Don't lose names in UState.universe_context.Gravatar Gaëtan Gilbert2017-09-19
| |/ |/| | | | | | | We dont care about the order of the binder map ([map] in the code) so no need to do tricky things with it.
* | Merge PR #1046: Better error messages, fix for BZ#5723Gravatar Maxime Dénès2017-09-15
|\ \
* \ \ Merge PR #1037: Parse directly to Sorts.family when appropriate.Gravatar Maxime Dénès2017-09-15
|\ \ \
* \ \ \ Merge PR #1002: Partial fix of BZ#5707 ("destruct" on primitive "negative" ↵Gravatar Maxime Dénès2017-09-15
|\ \ \ \ | | | | | | | | | | | | | | | Inductive-keyworded record failing even on non-dependent goal)
| | | | * Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Guillaume Melquiond2017-09-14
| |_|_|/ |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This changes the implementation of "constructor" from constructor 1 + ... + constructor n + fail to constructor 1 + ... + constructor n.
| | | * Better error messages, fix for BZ#5723Gravatar Paul Steckler2017-09-11
| |_|/ |/| |
| | * Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
| |/ |/| | | | | | | 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.
* | Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | 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.
| * Fixing part of #5707 (allowing destruct to use non dependent case analysis).Gravatar Hugo Herbelin2017-08-30
| | | | | | | | | | | | 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.
* | Fix BZ#5697: Congruence does not work with primitive projections.Gravatar Pierre-Marie Pédrot2017-08-29
| | | | | | | | | | The code generating the projection was unconditionally generating pattern-matchings, although this is incorrect for primitive records.
* | Merge PR #830: Moving assert (the "Cut" rule) to new proof engineGravatar Maxime Dénès2017-08-29
|\ \
* \ \ Merge PR #805: Functional tacticsGravatar Maxime Dénès2017-08-29
|\ \ \ | |_|/ |/| |
* | | Merge PR #928: Fixing bug #5671 (tactic specialize unclean wrt Metas).Gravatar Maxime Dénès2017-08-01
|\ \ \
* \ \ \ Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \ \ \
* \ \ \ \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \ \ \
| | | | * | better `try with` scope in `discr_positions`Gravatar amblaf2017-07-31
| | | | | |
| | | | * | Correcting [build_discriminator] to make the test-suite passGravatar amblaf2017-07-31
| | | | | |
| | | | * | Replacing tclENV with the goal environmentGravatar amblaf2017-07-31
| | | | | | | | | | | | | | | | | | | | | | | | In functions match_eqdec and check_unused_names
| | | | * | env, sigma as first arguments of functionsGravatar amblaf2017-07-31
| | | | | |
| | | | * | Remove references to Global.env in tactics/*.mlGravatar amblaf2017-07-31
| |_|_|/ / |/| | | | | | | | | | | | | | Only in ml files that are not related to Coq commands
* | | | | Merge PR #888: Stronger kernel typesGravatar Maxime Dénès2017-07-28
|\ \ \ \ \
| | | | * | Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| |_|_|/ / |/| | | |
| | * | | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | | | |
| | | * | Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| |_|/ / |/| | |
| * | | More precise type for universe entries.Gravatar Pierre-Marie Pédrot2017-07-26
| |/ / | | | | | | | | | | | | We use an algebraic type instead of a pair of a boolean and the corresponding data. For now, this is isomorphic, but this allows later change in the structure.
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 00:35:57 +0000