aboutsummaryrefslogtreecommitdiff
path: root/tactics/auto.mli
AgeCommit message (Expand)Author
2020-08-12Move connect_hint_clenv from Auto to Hints.Pierre-Marie Pédrot
2020-06-19Move the hint polymorphic status to the hint instance.Pierre-Marie Pédrot
2020-06-19Wrap the content of full hints into a record.Pierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2019-06-24[api] Remove `polymorphic` type alias, use labels instead.Emilio Jesus Gallego Arias
2019-06-17Update ml-style headers to new year.Théo Zimmermann
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-04-27Remove unused [open] statementsGaetan Gilbert
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Auto API using EConstr.Pierre-Marie Pédrot
2017-02-14Hints API using EConstr.Pierre-Marie Pédrot
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-04Merge remote-tracking branch 'github/pr/336' into v8.6Maxime Dénès
2016-10-29Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-25Remove v62 from the codebase.Théo Zimmermann
2016-10-21sections/hints: prevent Not_found in get_type_ofMatthieu Sozeau
2016-10-12Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-12Fix bug #4958: [debug auto] should specify hint databases.Pierre-Marie Pédrot
2016-09-15Untangling Tacexpr from lower strata.Pierre-Marie Pédrot
2016-09-08Unplugging Tacexpr in several interface files.Pierre-Marie Pédrot
2016-06-27Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-09Adding a bit of documentation in the mli.Pierre-Marie Pédrot
2016-06-09Univs/(e)auto: fix bug #4450 polymorphic exact hintsMatthieu Sozeau
2016-03-20Relying on generic arguments to represent Extern hints.Pierre-Marie Pédrot
2016-01-21Merge branch 'v8.5'Pierre-Marie Pédrot
2016-01-20Update copyright headers.Maxime Dénès
2016-01-02Reduce dependencies of interface files.Guillaume Melquiond
2015-12-28Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Pierre-Marie Pédrot
2015-10-29Removing unused and useless exported function in Hints.Pierre-Marie Pédrot
2015-10-20Indexing Proofview.goals with a stage.Pierre-Marie Pédrot
2015-10-16Generalize fix for auto from PMP to eauto and typeclasses eauto.Matthieu Sozeau
2015-10-14Exporting the original unprocessed hint in the hint running function.Pierre-Marie Pédrot
2015-05-11Rationalizing a bit the interface of Hints.Pierre-Marie Pédrot
2015-02-02Removing dead code.Pierre-Marie Pédrot
2015-01-12Update headers.Maxime Dénès
2014-10-15Remaining tactics of the Auto module were put in the monad.Pierre-Marie Pédrot
2014-10-07Splitting out of auto.ml a file hints.ml dedicated to hints so as toHugo Herbelin
2014-10-01Made Tacsubst independent of Auto at linking time so that Tacenv doesHugo Herbelin
2014-09-15Add a "Hint Mode ref (+ | -)*" hint for setting a global modeMatthieu Sozeau
2014-09-10A step towards better differentiating when w_unify is used for subtermHugo Herbelin
2014-05-06This commit adds full universe polymorphism and fast projections to Coq.Matthieu Sozeau
2014-03-05Remove many superfluous 'open' indicated by ocamlc -w +33Pierre Letouzey
2013-11-02Makes the new Proofview.tactic the basic type of Ltac.aspiwack
2013-09-03Some cleanup in Autoppedrot
2013-07-17Pre-create typeclass_instances and rewrite hintdb in Autoletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 09:52:07 +0000