aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Expand)Author
2018-11-20Merge PR #7925: Clean transparent stateMaxime Dénès
2018-11-19Rename TranspState into TransparentState.Pierre-Marie Pédrot
2018-11-19Proper record type and accessors for transparent states.Pierre-Marie Pédrot
2018-11-19Move transparent_state to its own module.Pierre-Marie Pédrot
2018-11-14Deprecate hint declaration/removal with no specified databaseMaxime Dénès
2018-10-19Deprecating Global.type_of_global_in_context.Hugo Herbelin
2018-10-16Simplify vars_of_global usageGaëtan Gilbert
2018-10-10[coqlib] Rebindable Coqlib namespace.Emilio Jesus Gallego Arias
2018-10-06[api] Remove (most) 8.9 deprecated objects.Emilio Jesus Gallego Arias
2018-10-05[kernel] Remove section paths from `KerName.t`Maxime Dénès
2018-09-26Make the warning for non-imported hints compatible with internal backtracking.Pierre-Marie Pédrot
2018-09-19Replace trivial uses of declare_summary with summary.refsGaëtan Gilbert
2018-09-19Remove Hints.add_hints_initGaëtan Gilbert
2018-09-12Move maps & sets indexed by GlobRef.t into the kernelVincent Laporte
2018-07-25Hints use Declare to declare universes instead of a custom object.Gaëtan Gilbert
2018-07-24Projections use index representationGaëtan Gilbert
2018-07-02hints: add Hint Variables/Constants Opaque/Transparent commandsMatthieu Sozeau
2018-06-25Clarify the message "this hint will only be used by eauto"Armaël Guéneau
2018-06-18Remove reference name type.Maxime Dénès
2018-06-04Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Pierre-Marie Pédrot
2018-06-04Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...Pierre-Marie Pédrot
2018-06-04Merge PR #7640: Small refactoring to clarify make_local_hint_db.Pierre-Marie Pédrot
2018-06-03Cleaning, documentation, uniformisation of the Coq extension of List.Hugo Herbelin
2018-06-01Merge PR #7234: Reduce circular dependency constants <-> projectionsMaxime Dénès
2018-05-31Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Armaël Guéneau
2018-05-31Merge PR #6969: [api] Remove functions deprecated in 8.8Maxime Dénès
2018-05-31Reduce circular dependency constants <-> projectionsGaëtan Gilbert
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-30Merge PR #7558: [api] Make `vernac/` self-contained.Maxime Dénès
2018-05-30Small refactoring to clarify make_local_hint_db.Théo Zimmermann
2018-05-27[api] Make `vernac/` self-contained.Emilio Jesus Gallego Arias
2018-05-27[tactics] Turn boolean locality hint parameter into a named one.Emilio Jesus Gallego Arias
2018-05-25Remove some occurrences of Evd.emptyMaxime Dénès
2018-05-23Moving Option.smart_map to Option.Smart.map.Hugo Herbelin
2018-05-23Collecting List.smart_* functions into a module List.Smart.Hugo Herbelin
2018-05-17Split off Universes functions dealing with generating new universes.Gaëtan Gilbert
2018-05-04[api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Emilio Jesus Gallego Arias
2018-04-26[api] Move `hint_info_expr` to `Typeclasses`.Emilio Jesus Gallego Arias
2018-03-31[econstr] Forbid calling `to_constr` in open terms.Emilio Jesus Gallego Arias
2018-03-09[located] Push inner locations in `reference` to a CAst.t node.Emilio Jesus Gallego Arias
2018-03-05Merge PR #6855: Update headers following #6543.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
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-11-19[proof] Attempt to deprecate some V82 parts of the proof API.Emilio Jesus Gallego Arias
2017-11-06[api] Move structures deprecated in the API to the core.Emilio Jesus Gallego Arias
2017-09-11Better error messages, fix for BZ#5723Paul Steckler
2017-07-13Remove the function Global.type_of_global_unsafe.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-18 05:40:25 +0000