aboutsummaryrefslogtreecommitdiff
path: root/tactics/class_tactics.ml
AgeCommit message (Expand)Author
2020-05-16Factorize code in hint declaration.Pierre-Marie Pédrot
2020-05-14[exn] [tactics] improve backtraces on monadic errorsEmilio Jesus Gallego Arias
2020-04-21Merge PR #11896: Use lists instead of arrays in evar instances.Maxime Dénès
2020-04-06Clean and fix definitions of options.Théo Zimmermann
2020-04-06Use lists instead of arrays in evar instances.Pierre-Marie Pédrot
2020-03-19Merge PR #11735: Deprecating catchable_exceptionPierre-Marie Pédrot
2020-03-18Update headers in the whole code base.Théo Zimmermann
2020-03-13Implementing postponed constraints in TC resolutionMatthieu Sozeau
2020-03-13Fixing a non-protected try-with in class_tactics.ml.Hugo Herbelin
2020-03-13Removing catchable_exception test in tclOR/tclORELSE.Hugo Herbelin
2020-03-05Merge PR #7791: Deprecating the declaration of arbitrary terms as hints.Maxime Dénès
2020-03-03[exninfo] Deprecate aliases for exception re-raising.Emilio Jesus Gallego Arias
2020-02-28Deprecate the OCaml API to declare term Hints.Pierre-Marie Pédrot
2020-02-12Remove Goptions.opt_name fieldGaëtan Gilbert
2020-02-06unsafe_type_of -> get_type_of in Class_tactics.autoapplyGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-08-17Delay the computation of frozen evars in legacy unification.Pierre-Marie Pédrot
2019-07-11Merge PR #10498: [api] Deprecate GlobRef constructors.Gaëtan Gilbert
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-08[core] [api] Support OCaml 4.08Emilio Jesus Gallego Arias
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
2019-05-02Remove outdated commentMaxime Dénès
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
2019-04-10Functionalize env in type classesMaxime Dénès
2019-04-02Merge PR #8984: Declare initial hint databases in preludePierre-Marie Pédrot
2019-03-27[tactic] Adapt tactic layer to removal of imperative proof state.Emilio Jesus Gallego Arias
2019-03-26Declare initial hint databases in preludeMaxime Dénès
2019-03-12Merge PR #7819: Ho matching occ selEnrico Tassi
2019-02-12[tactics] Remove dependency of abstract on global proof state.Emilio Jesus Gallego Arias
2019-02-08Change interfaces of evarconv as suggested by Enrico.Matthieu Sozeau
2019-02-08[evarconv] New flag handling for unifierMatthieu Sozeau
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-27 11:09:53 +0000