aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
AgeCommit message (Expand)Author
2018-10-26[typeclasses] functionalize typeclass evar handlingMatthieu Sozeau
2018-10-26Cleanup evar_extra: remove evar_info's store and add maps to evar_mapMatthieu Sozeau
2018-10-01Merge PR #8177: Make the warning for non-imported hints compatible with inter...Matthieu Sozeau
2018-09-26[print] Restrict use of "debug" Termops printer.Emilio Jesus Gallego Arias
2018-09-26Make the warning for non-imported hints compatible with internal backtracking.Pierre-Marie Pédrot
2018-09-24[engine] Remove and deprecate `nf_enter` et al.Emilio Jesus Gallego Arias
2018-06-26Remove Sorts.contentsGaëtan Gilbert
2018-06-12[api] Misctypes removal: tactic flags.Emilio Jesus Gallego Arias
2018-06-07Merge PR #7629: Fix anomaly in autoapply when an unbound hint name is providedMatthieu Sozeau
2018-05-31Remove some dead code in class_tactics.mlArmaël Guéneau
2018-05-31Merge PR #6969: [api] Remove functions deprecated in 8.8Maxime Dénès
2018-05-30Move interning the [hint_pattern] outside the Typeclasses hooks.Gaëtan Gilbert
2018-05-30[api] Remove deprecated object from `Term`Emilio Jesus Gallego Arias
2018-05-29Fix anomaly in autoapply when an unbound hint name is providedArmaël Guéneau
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
2018-04-13Evar maps contain econstrs.Gaëtan Gilbert
2018-03-08Add an invariant on given up goals in class_tactics.Hugo Herbelin
2018-03-08Proof engine: support for nesting tactic-in-term within other tactics.Hugo Herbelin
2018-03-08Proof engine: consider the pair principal and future goals as an entity.Hugo Herbelin
2018-03-06Merge PR #6824: Remove deprecated options related to typeclasses.Maxime Dénès
2018-03-05Merge PR #6855: Update headers following #6543.Maxime Dénès
2018-03-04Remove deprecated options related to typeclasses.Théo Zimmermann
2018-03-04Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Maxime Dénès
2018-02-28[econstr] Continue consolidation of EConstr API under `interp`.Emilio Jesus Gallego Arias
2018-02-27Update headers following #6543.Théo Zimmermann
2018-02-20proofview: goals come with a stateEnrico Tassi
2018-02-12[engine] Remove ghost parameter from `Proofview.Goal.t`Emilio Jesus Gallego Arias
2018-01-02Cleanup name-binding structure for fresh evar name generation.Pierre-Marie Pédrot
2017-12-11[proof] Embed evar_map in RefinerError exception.Emilio Jesus Gallego Arias
2017-11-21[printing] Deprecate all printing functions accessing the global proof.Emilio Jesus Gallego Arias
2017-08-29Merge PR #805: Functional tacticsMaxime Dénès
2017-08-01Merge PR #919: Remove a few useless evar-normalizations in printing code.Maxime Dénès
2017-07-31Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadMaxime Dénès
2017-07-31env, sigma as first arguments of functionsamblaf
2017-07-31Remove references to Global.env in tactics/*.mlamblaf
2017-07-27deprecate Pp.std_ppcmds type aliasMatej Košík
2017-07-26Remove a few useless evar-normalizations in printing code.Pierre-Marie Pédrot
2017-07-26Merge PR #868: Fix debug trace of typeclasses eauto.Maxime Dénès
2017-07-20Merge PR #892: Improve do_split option of typeclass resolutionMaxime Dénès
2017-07-20Merge PR #869: Enforce alternating separators in typeclass debug outputMaxime Dénès
2017-07-19Fix debug trace of typeclasses eauto.Théo Zimmermann
2017-07-18Improve do_split option of typeclass resolutionMatthieu Sozeau
2017-07-12format pairs of items for pr_depth to get alternating separatorsPaul Steckler
2017-07-11Deprecate options that were introduced for compatibility with 8.5.Théo Zimmermann
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-19Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalMaxime Dénès
2017-06-19Merge PR#727: [tactics] Fix summary registration of global hint variable.Maxime Dénès
2017-06-14[typeclasses eauto] Fix bug #3943: non-termination in topologicalMatthieu Sozeau
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 15:26:58 +0000