aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.mli
Commit message (Collapse)AuthorAge
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | Fixing rewriting in side conditions for "rewrite in *" and "rewrite in * |-".Gravatar Hugo Herbelin2018-03-01
| | | | | | | | Noticed by Sigurd Schneider.
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [engine] Remove ghost parameter from `Proofview.Goal.t`Gravatar Emilio Jesus Gallego Arias2018-02-12
| | | | | | | | | | | | | | In current code, `Proofview.Goal.t` uses a phantom type to indicate whether the goal was properly substituted wrt current `evar_map` or not. After the introduction of `EConstr`, this distinction should have become unnecessary, thus we remove the phantom parameter from `'a Proofview.Goal.t`. This may introduce some minor incompatibilities at the typing level. Code-wise, things should remain the same. We thus deprecate `assume`. In a next commit, we will remove normalization as much as possible from the code.
* [API] remove large file containing duplicate interfacesGravatar Enrico Tassi2017-12-27
| | | | | ... in favor of having Public/Internal sub modules in each and every module grouping functions according to their intended client.
* [api] Insert miscellaneous API deprecation back to core.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 Name.Id in core.Gravatar Emilio Jesus Gallego Arias2017-11-04
| | | | This is a first step towards some of the solutions proposed in #6008.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | Reminder of (some of) the reasons for removal: - Despite the claim in sigma.mli, it does *not* prevent evar leaks, something like: fun env evd -> let (evd',ev) = new_evar env evd in (evd,ev) will typecheck even with Sigma-like type annotations (with a proof of reflexivity) - The API stayed embryonic. Even typing functions were not ported to Sigma. - Some unsafe combinators (Unsafe.tclEVARS) were replaced with slightly less unsafe ones (e.g. s_enter), but those ones were not marked unsafe at all (despite still being so). - There was no good story for higher order functions manipulating evar maps. Without higher order, one can most of the time get away with reusing the same name for the updated evar map. - Most of the code doing complex things with evar maps was using unsafe casts to sigma. This code should be fixed, but this is an orthogonal issue. Of course, this was showing a nice and elegant use of GADTs, but the cost/benefit ratio in practice did not seem good.
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
| | | | | | | | Now it is a private field, locations are optional.
| * Fix the API of the new pf_constr_of_global.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | | | | | | | The current implementation was still using continuation passing-style, and furthermore was triggering a focus on the goals. We take advantage of the tactic features instead.
| * Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
| | | | | | | | | | | | The only remaining use was applied on the unfold tactic, and the behaviours of tclPROGRESS and tclWEAK_PROGRESS coincide whenever only one goal is produced by their argument tactic.
| * Removing the tclNOTSAMEGOAL primitive from the API.Gravatar Pierre-Marie Pédrot2017-04-24
|/ | | | The only use in Equality is reimplemented in the new engine.
* Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
| | | | | | The transition has been done a bit brutally. I think we can still save a lot of useless normalizations here and there by providing the right API in EConstr. Nonetheless, this is a first step.
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | Now they are useless because all of the primitives are (should?) be evar-insensitive.
* | Do not ask for a normalized goal to get hypotheses and conclusions.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | This is now useless as this returns evar-constrs, so that all functions acting on them should be insensitive to evar-normalization.
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | | | This removes quite a few unsafe casts. Unluckily, I had to reintroduce the old non-module based names for these data structures, because I could not reproduce easily the same hierarchy in EConstr.
* | Removing compatibility layers from TacticalsGravatar Pierre-Marie Pédrot2017-02-14
| |
* | Cleaning up interfaces.Gravatar Pierre-Marie Pédrot2017-02-14
| | | | | | | | | | We make mli files look to what they were looking before the move to EConstr by opening this module.
* | Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Tacticals API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Proofview: tclINDEPENDENTLGravatar Enrico Tassi2017-02-10
|/
* Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
|
* Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| | | | | | | | | | | | This allows to write things like this: split; 2: intro _; exact I or like this: eexists ?[x]; ?[x]: exact 0; trivial This has the side-effect on making the '?' before '[x]' mandatory.
* Tacticals: typo in a commentGravatar Pierre Letouzey2016-02-16
|
* New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
| | | | | - Fixing dead code, doc. - Relaxing constraints on using an as-tuple in inversion.
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
| | | | | | | | | | | | | | | | | | | | The length of the pattern should now be exactly the number of assumptions and definitions introduced by the destruction or induction, including the induction hypotheses in case of an induction. Like for pattern-matching, the local definitions in the argument of the constructor can be skipped in which case a name is automatically created for these.
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| |
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | The structure of the Context module was refined in such a way that: - Types and functions related to rel-context declarations were put into the Context.Rel.Declaration module. - Types and functions related to rel-context were put into the Context.Rel module. - Types and functions related to named-context declarations were put into the Context.Named.Declaration module. - Types and functions related to named-context were put into the Context.Named module. - Types and functions related to named-list-context declarations were put into Context.NamedList.Declaration module. - Types and functions related to named-list-context were put into Context.NamedList module. Some missing comments were added to the *.mli file. The output of ocamldoc was checked whether it looks in a reasonable way. "TODO: cleanup" was removed The order in which are exported functions listed in the *.mli file was changed. (as in a mature modules, this order usually is not random) The order of exported functions in Context.{Rel,Named} modules is now consistent. (as there is no special reason why that order should be different) The order in which are functions defined in the *.ml file is the same as the order in which they are listed in the *.mli file. (as there is no special reason to define them in a different order) The name of the original fold_{rel,named}_context{,_reverse} functions was changed to better indicate what those functions do. (Now they are called Context.{Rel,Named}.fold_{inside,outside}) The original comments originally attached to the fold_{rel,named}_context{,_reverse} did not full make sense so they were updated. Thrown exceptions are now documented. Naming of formal parameters was made more consistent across different functions. Comments of similar functions in different modules are now consistent. Comments from *.mli files were copied to *.ml file. (We need that information in *.mli files because that is were ocamldoc needs it. It is nice to have it also in *.ml files because when we are using Merlin and jump to the definion of the function, we can see the comments also there and do not need to open a different file if we want to see it.) When we invoke ocamldoc, we instruct it to generate UTF-8 HTML instead of (default) ISO-8859-1. (UTF-8 characters are used in our ocamldoc markup) "open Context" was removed from all *.mli and *.ml files. (Originally, it was OK to do that. Now it is not.) An entry to dev/doc/changes.txt file was added that describes how the names of types and functions have changed.
* | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
|/ / | | | | | | | | | | | | | | | | | | | | The previous implementation was a source of evar leaks if misused, as it created values coming together with their current evar_map. This is dead wrong if the value is not used on the spot. To fix this, we rather return a ['a delayed_open] object. Two argument types were modified: bindings and constr_bindings. The open_constr argument should also be fixed, but it is more entangled and thus I leave it for another commit.
* / Indexing Proofview.goals with a stage.Gravatar Pierre-Marie Pédrot2015-10-20
|/ | | | | | This is not perfect though, some primitives are unsound, and some higher-order API should use polymorphic functions so as not to depend on a given level.
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
|
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
|
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
| | | | | | | | | | | | | | | | | | | | Instead of modifying exceptions to wear additional information, we instead use a dedicated type now. All exception-using functions were modified to support this new type, in particular Future's fix_exn-s and the tactic monad. To solve the problem of enriching exceptions at raise time and recover this data in the try-with handler, we use a global datastructure recording the given piece of data imperatively that we retrieve in the try-with handler. We ensure that such instrumented try-with destroy the data so that there may not be confusion with another exception. To further harden the correction of this structure, we also check for pointer equality with the last raised exception. The global data structure is not thread-safe for now, which is incorrect as the STM uses threads and enriched exceptions. Yet, we splitted the patch in two parts, so that we do not introduce dependencies to the Thread library immediatly. This will allow to revert only the second patch if ever we switch to OCaml-coded lightweight threads.
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
| | | | [tryif t then t2 else t3] behaves like [t;t2] if [t] has at least one success, or [t3] otherwise. It generalises [t||t3] as failures from [t2] will not be caught.
* Constructor tactics backtracking is done using [Tacticals.New] rather than ↵Gravatar Arnaud Spiwack2014-12-08
| | | | | | | | | [Proofview]. The primitives in [Tacticals] respect Ltac's error level, whereas the one in [Proofview] do not necessarily. In that case the error caught was ignored causing arbitrary error level after [constructor] to be canceled. Needed the addition of an [ORD] variant to [OR] in [Tacticals.New] to avoid unnecessary precomputation (the 'D' stands for 'delay'). Fixes #3838.
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
|
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
| | | | | | | can be given with second H bound by the first one. Not very satisfied by passing closure to tactics.ml, but otherwise tactics would have to be aware of glob_constr.
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
| | | | "pat/term" for "apply term on current_hyp as pat".
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
| | | | | | | | | | | | | | | | - emphasizing the different kinds of patterns - factorizing code of the non-naming intro-patterns Still some questions: - Should -> and <- apply to hypotheses or not (currently they apply to hypotheses either when used in assert-style tactics or apply in, or when the term to rewrite is a variable, in which case "subst" is applied)? - Should "subst" be used when the -> or <- rewrites an equation x=t posed by "assert" (i.e. rewrite everywhere and clearing x and hyp)? - Should -> and <- be applicable in non assert-style if the lemma has quantifications?
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
| | | | backtracks, print time spent in each of successive calls.
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
| | | | This reverts commit abad0a15ac44cb5b53b87382bb4d587d9800a0f6.