aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.mli
Commit message (Expand)AuthorAge
* 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
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* 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
* | 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
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\|
| * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
* | 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
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* 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
| |/
* / 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
* 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
* Fix CFGV contrib: handling of global hints introducing global universes.Gravatar Matthieu Sozeau2015-10-09
* 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
* 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
* Update headers.Gravatar Maxime Dénès2015-01-12
* Forgotten hints.ml{,i} files in 38b34dfffcc.Gravatar Hugo Herbelin2014-10-08