aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
AgeCommit message (Expand)Author
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-04Document undocumented flags and optionsJim Fehrle
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
2018-11-23Goptions.declare_* functions return unit instead of a write_functionGaëtan Gilbert
2018-11-20Merge PR #8982: [proof] Provide better control of "open proofs" exceptions.Pierre-Marie Pédrot
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-19[proof] Provide better control of "open proofs" exceptions.Emilio Jesus Gallego Arias
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-19 06:43:39 +0000