aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.ml
Commit message (Collapse)AuthorAge
...
* Reductionops.nf_* now take an environment.Gravatar Gaëtan Gilbert2018-02-02
|
* [api] Also deprecate constructors of Decl_kinds.Gravatar Emilio Jesus Gallego Arias2017-12-23
| | | | | | | | Unfortunately OCaml doesn't deprecate the constructors of a type when the type alias is deprecated. In this case it means that we don't get rid of the kernel dependency unless we deprecate the constructors too.
* Merge PR #6169: Clean up/deprecated optionsGravatar Maxime Dénès2017-12-14
|\
* \ Merge PR #6038: [build] Remove coqmktop in favor of ocamlfind.Gravatar Maxime Dénès2017-12-14
|\ \
* | | [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | The exception needs to carry aroud a pair of `env, sigma` so printing is correct. This gets rid of a few global calls, and it is IMO the right thing to do. While we are at it, we incorporate some fixes to a couple of additional printing functions missing the `env, sigma` pair.
| | * Remove deprecated option Tactic Compat Context.Gravatar Théo Zimmermann2017-12-11
| | | | | | | | | | | | And some code simplification.
| | * Remove deprecated option Dependent Propositions Eliminiation.Gravatar Théo Zimmermann2017-12-11
| |/ |/| | | | | And a bit of code simplification.
| * [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
|/ | | | | New module introduced in OCaml 4.05 I think, can create problems when linking with the OCaml toplevel for `Drop`.
* [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.
* [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.
* [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
|\
| * 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 #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.
* Merge PR #1050: Avoid extra failure in the "constructor" tactic (bug #5666).Gravatar Maxime Dénès2017-09-19
|\
* \ 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.
| * 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.
* | 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
|\ \ \
| | * | Replacing tclENV with the goal environmentGravatar amblaf2017-07-31
| | | | | | | | | | | | | | | | In functions match_eqdec and check_unused_names
| | * | Remove references to Global.env in tactics/*.mlGravatar amblaf2017-07-31
| |/ / |/| | | | | | | | Only in ml files that are not related to Coq commands
| * | Fixing bug #5671 (specialize unclean wrt Metas).Gravatar Hugo Herbelin2017-07-27
| | |
* | | 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 branch 'v8.7'Gravatar Maxime Dénès2017-07-20
|\ \
* | | 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.
* | | Safer API for constr_of_global, and getting rid of unsafe_constr_of_global.Gravatar Pierre-Marie Pédrot2017-07-13
| | |
| * | Backtracking on deprecation of Bracketing Last Intro Pattern.Gravatar Théo Zimmermann2017-07-11
| | | | | | | | | | | | | | | | | | As per @JasonGross's request who described a use case for this option in https://coq.inria.fr/bugs/show_bug.cgi?id=5633 and pending an alternative solution for this use case.
| * | Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
|/ /
* | Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
| |
| * Reorganizing functions to find the relative position of an hypothesis.Gravatar Hugo Herbelin2017-06-25
| | | | | | | | | | Also fixing a bug of get_next_hyp_position when the hypothesis is the oldest of the context (see test in ltac.v).
| * Moving "assert" (internally "Cut") to the new proof engine.Gravatar Hugo Herbelin2017-06-25
|/ | | | | It allows in particular to have "Info" on tactic "assert" and derivatives not to give an "<unknown>".
* Merge PR#375: DeprecationGravatar Maxime Dénès2017-06-15
|\
* \ Merge PR#763: [proof] Deprecate redundant wrappers.Gravatar Maxime Dénès2017-06-14
|\ \
| | * Deprecate options that were introduced for compatibility with 8.4.Gravatar Guillaume Melquiond2017-06-14
| | |
| | * Deprecate options that were introduced for compatibility with 8.2.Gravatar Guillaume Melquiond2017-06-14
| | |
| | * Remove support for Coq 8.4.Gravatar Guillaume Melquiond2017-06-14
| | |
| | * Remove support for Coq 8.2.Gravatar Guillaume Melquiond2017-06-14
| | |
* | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| | |
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 09:58:37 +0000