aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/auto.ml
Commit message (Expand)AuthorAge
* Clean-up remove always false useeager argument.Gravatar Théo Zimmermann2018-03-06
* 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
* [lib] Rename Profile to CProfileGravatar Emilio Jesus Gallego Arias2017-12-09
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Fixing bug #5741 (anomaly in info_trivial).Gravatar Hugo Herbelin2017-09-19
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#638: Fix bug #5360: anomalies in typeclass resolution outputGravatar Maxime Dénès2017-06-06
|\
* | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * Fix bug #5360: anomalies in typeclass resolution outputGravatar Matthieu Sozeau2017-05-16
|/
* Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
* Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\
* | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Ltac now uses evar-based constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Auto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
| * Tests for info/debug auto/eauto.Gravatar Hugo Herbelin2016-11-19
|/
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Merge remote-tracking branch 'github/pr/321' into v8.6Gravatar Maxime Dénès2016-10-28
| |\
| * | Using msg_info for info_auto and info_eauto (PR #324).Gravatar Hugo Herbelin2016-10-26
| | * sections/hints: prevent Not_found in get_type_ofGravatar Matthieu Sozeau2016-10-21
| |/
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-17
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-10-17
| |\
| | * Still a problem with debug auto printing.Gravatar Hugo Herbelin2016-10-15
| | * One more little bug in the output of "debug auto".Gravatar Hugo Herbelin2016-10-15
| | * Fixing printing of info_auto broken since 0091c528 (2014).Gravatar Hugo Herbelin2016-10-14
| * | Fixing English typography for colon.Gravatar Hugo Herbelin2016-10-14
* | | 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
* | | Merging Stdarg and Constrarg.Gravatar Pierre-Marie Pédrot2016-09-21
* | | Unplugging Tacexpr in several interface files.Gravatar Pierre-Marie Pédrot2016-09-08
|/ /
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\|
| * Univs/(e)auto: fix bug #4450 polymorphic exact hintsGravatar Matthieu Sozeau2016-06-09
* | Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* | Removing external uses of Val.inject and making Geninterp.interp return Val.tGravatar Pierre-Marie Pédrot2016-05-04
* | Getting rid of the Geninterp.generic_interp function.Gravatar Pierre-Marie Pédrot2016-05-04
* | Switching to an untyped toplevel representation for Ltac values.Gravatar Pierre-Marie Pédrot2016-05-04
* | Relying on generic arguments to represent Extern hints.Gravatar Pierre-Marie Pédrot2016-03-20