aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Expand)Author
2019-12-16Pretyping.check_evars: make initial evar map optionalGaëtan Gilbert
2019-11-21[coq] Untabify the whole ML codebase.Emilio Jesus Gallego Arias
2019-11-11Do not export the internals of the prepare_hint function.Pierre-Marie Pédrot
2019-07-08[api] Deprecate GlobRef constructors.Emilio Jesus Gallego Arias
2019-07-01[declare] Remove superfluous APIEmilio Jesus Gallego Arias
2019-07-01[declare] Separate kinds from entries in constant declarationEmilio Jesus Gallego Arias
2019-06-25Remove the internal_flag argument from Declare API.Pierre-Marie Pédrot
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-06-09[proof] Move proofs that have an associated constant to `Lemmas`Emilio Jesus Gallego Arias
2019-05-02Fix #5752: `Hint Mode` ignored for type classes that appear as assumptionsMaxime Dénès
2019-05-02Use GlobRef.Map.t in hint databasesMaxime Dénès
2019-04-10Remove calls to global env in InductiveopsMaxime Dénès
2019-04-10Remove calls to Global.env in PatternopsMaxime Dénès
2019-04-10Remove one call to Global.env in DetypingMaxime 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-20Stop accessing proof env via Pfedit in printersMaxime Dénès
2019-03-14Add relevance marks on binders.Gaëtan Gilbert
2019-02-17Separate variance and universe fields in inductives.Gaëtan Gilbert
2018-12-14[proof] Rework proof interface.Emilio Jesus Gallego Arias
2018-12-12Merge PR #8974: Fix mod_subst wrt universe polymorphismMaxime Dénès
2018-12-09[doc] Enable Warning 50 [incorrect doc comment] and fix comments.Emilio Jesus Gallego Arias
2018-12-05Fix mod_subst wrt universe polymorphismGaëtan Gilbert
2018-11-23s/let _ =/let () =/ in some places (mostly goptions related)Gaëtan Gilbert
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:46:38 +0000