aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Collapse)AuthorAge
* 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.
* | | Merge PR #868: Fix debug trace of typeclasses eauto.Gravatar Maxime Dénès2017-07-26
|\ \ \ | |/ / |/| |
* | | Merge PR #892: Improve do_split option of typeclass resolutionGravatar Maxime Dénès2017-07-20
|\ \ \
* \ \ \ Merge PR #899: [general] Move files to directories so they match linking order.Gravatar Maxime Dénès2017-07-20
|\ \ \ \
* \ \ \ \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \ \ \ \
* \ \ \ \ \ Merge branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \ \ \ \ \
| | | * | | | [general] Move files to directories matching linking order.Gravatar Emilio Jesus Gallego Arias2017-07-19
| |_|/ / / / |/| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | We move a bunch of modules (`Impargs`, `Declare`, `Ind_tables`, `Miscprint`) to their proper place as they were declared in different `mllib` files than the one in their directory. In some cases this could be refined but we don't do anything fancy, we just reflect the status quo.
| | | | * | Fix debug trace of typeclasses eauto.Gravatar Théo Zimmermann2017-07-19
| |_|_|/ / |/| | | |
| | | * | Improve do_split option of typeclass resolutionGravatar Matthieu Sozeau2017-07-18
| |_|/ / |/| | | | | | | | | | | | | | | It used to compute the dependencies of all undefined evars of the evar_map, while only the dependencies of resolvable evars are necessary.
* | | | Getting rid of abstraction breaking code in tclABSTRACT.Gravatar Pierre-Marie Pédrot2017-07-14
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This is probably the hardest case of them all, because tclABSTRACT fundamentally relies on the names of universes from the constant instance being the same as the one in the current goal. Adding to that the fact that the kernel is doing strange things when provided with a polymorphic definition with body universe constraints, it turns out to be a hellish nightmare to handle properly. At some point we need to clarifiy this in the kernel as well, although we leave it for some other patch.
* | | | Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
| | | |
* | | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | | |
* | | | Getting rid of AUContext abstraction breakers in Elimschemes.Gravatar Pierre-Marie Pédrot2017-07-13
| | | |
| | * | format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| | | | | | | | | | | | | | | | | | | | eval thunks once in prlist_sep_lastsep, make code clearer add typeclass debug output test
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-11 06:44:04 +0000