aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.mli
Commit message (Collapse)AuthorAge
* hints: add Hint Variables/Constants Opaque/Transparent commandsGravatar Matthieu Sozeau2018-07-02
| | | | | | | | | | | This gives user control on the transparent state of a hint db. Can override defaults more easily (report by J. H. Jourdan). For "core", declare that variables can be unfolded, but no constants (ensures compatibility with previous auto which allowed conv on closed terms) Document Hint Variables
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
| | | | | | | | reference was defined as Ident or Qualid, but the qualid type already permits empty paths. So we had effectively two representations for unqualified names, that were not seen as equal by eq_reference. We remove the reference type and replace its uses by qualid.
* Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
|
* Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| | | | | | Close #7562. [api] move hint_info ast to tactics.
* [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| | | | | | | | | | | | | | | | | | | | We make the vernacular implementation self-contained in the `vernac/` directory. To this extent we relocate the parser, printer, and AST to the `vernac/` directory, and move a couple of hint-related types to `Hints`, where they do indeed belong. IMO this makes the code easier to understand, and provides a better modularity of the codebase as now all things under `tactics` have 0 knowledge about vernaculars. The vernacular extension machinery has also been moved to `vernac/`, this will help when #6171 [proof state cleanup] is completed along with a stronger typing for vernacular interpretation that can distinguish different types of effects vernacular commands can perform. This PR introduces some very minor source-level incompatibilities due to a different module layering [thus deprecating is not possible]. Impact should be relatively minor.
* [tactics] Turn boolean locality hint parameter into a named one.Gravatar Emilio Jesus Gallego Arias2018-05-27
|
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
| | | | | | | | | | | | | In #6092, `global_reference` was moved to `kernel`. It makes sense to go further and use the current kernel style for names. This has a good effect on the dependency graph, as some core modules don't depend on library anymore. A question about providing equality for the GloRef module remains, as there are two different notions of equality for constants. In that sense, `KerPair` seems suspicious and at some point it should be looked at.
* [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
| | | | | | `hint_info_expr`, `hint_info_gen` do conceptually belong to the typeclasses modules and should be able to be used without a dependency on the concrete vernacular syntax.
* Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|
* [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] 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.
* deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
|
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
|
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
|
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | 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.
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| |
| * Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-12-07
| |\
| | * Fix bug #5232: proper globalization of hints pathsGravatar Matthieu Sozeau2016-11-30
| | |
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-11-18
|/| | | |/
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| | | | | | | | | | | | | | | | | | In addition to a priority, cleanup the interfaces for passing this information as well. The pattern, if given, takes priority over the inferred one. We only allow Existing Instances gr ... gr | pri. for now, without pattern, as before. Make the API compatible to 8.5 as well.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| | | | | | | | | | | | | | | | due to cleared/reverted section variables. This fixes the get_type_of but requires keeping information around about the section hyps available in goals during resolution. It's optimized for the non-section case (should incur no cost there), and the case where no section variables are cleared.
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\|
| * Fix bug #4958: [debug auto] should specify hint databases.Gravatar Pierre-Marie Pédrot2016-10-12
| |
* | Untangling Tacexpr from lower strata.Gravatar Pierre-Marie Pédrot2016-09-15
| |
* | Making Hints generic in the use of external tactics.Gravatar Pierre-Marie Pédrot2016-09-08
| |
* | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
| |
* | Making Vernacexpr independent from Tacexpr.Gravatar Pierre-Marie Pédrot2016-09-08
|/
* Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
| | | | | | | Suggested by R. Krebbers and C. Cohen, this makes modes more applicable, by allowing to trigger resolution on partially instantiated indices. This is a rough but fast approximation of the pattern on which one would like instances to apply.
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
| | | | | As noticed by C. Cohen it was confusingly different from standard notation.
* Relying on generic arguments to represent Extern hints.Gravatar Pierre-Marie Pédrot2016-03-20
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\
| * 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.
* / Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
|/
* Hint Cut documentation and cleanup of printing (was duplicated andGravatar Matthieu Sozeau2015-11-04
| | | | inconsistent).
* Exporting the original unprocessed hint in the hint running function.Gravatar Pierre-Marie Pédrot2015-10-14
|
* Refine fix for handling of the universe contexts of hints, depending onGravatar Matthieu Sozeau2015-10-09
| | | | their polymorphic status _and_ locality.
* Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
| | | | It was wrong, the context was readded needlessly to the local evar_map context.
* Fix bug #4354: interpret hints in the right env and sigma.Gravatar Matthieu Sozeau2015-10-06
|
* Rationalizing a bit the interface of Hints.Gravatar Pierre-Marie Pédrot2015-05-11
|
* Opaque implementation of auto tactics.Gravatar Pierre-Marie Pédrot2015-04-14
| | | | | | We provide an eliminator ensuring that the AST will be used to build a tactic, so that we can stuff arbitrary things inside. An escape function is also provided for backward compatibility.
* Making the hint entry type opaque.Gravatar Pierre-Marie Pédrot2015-04-12
|
* Making the hints for the auto tactics private.Gravatar Pierre-Marie Pédrot2015-04-10
| | | | | | They are all generated by the Hints module, and making them purely opaque is not worthwhile because we project them a lot. This ensures that they all get generated following a uniform process.
* Update headers.Gravatar Maxime Dénès2015-01-12
|
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08