aboutsummaryrefslogtreecommitdiff
path: root/tactics/hints.ml
AgeCommit message (Expand)Author
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
2017-07-04Bump year in headers.Pierre-Marie Pédrot
2017-06-16Clean up universes of constants and inductivesAmin Timany
2017-06-11[proof] Deprecate redundant wrappers.Emilio Jesus Gallego Arias
2017-06-06Remove the Sigma (monotonous state) API.Maxime Dénès
2017-06-02Drop '.' from CErrors.anomaly, insert it in argsJason Gross
2017-05-27[cleanup] Unify all calls to the error function.Emilio Jesus Gallego Arias
2017-05-25Merge PR#608: Allow Ltac2 as a pluginMaxime Dénès
2017-05-25Merge PR#481: [option] Remove support for non-synchronous options.Maxime Dénès
2017-05-24Merge branch 'trunk' into located_switchEmilio Jesus Gallego Arias
2017-05-24[option] Remove support for non-synchronous options.Emilio Jesus Gallego Arias
2017-05-03Allowing to pass arbitrary data in internalization environments.Pierre-Marie Pédrot
2017-05-02Remove unused module definition after merging PR#592.Maxime Dénès
2017-05-02Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.Maxime Dénès
2017-04-30Fix bug #5501: Universe polymorphism breaks proof involving auto.Pierre-Marie Pédrot
2017-04-27Fix omitted labels in function callsGaetan Gilbert
2017-04-25[location] Make location optional in Loc.locatedEmilio Jesus Gallego Arias
2017-04-21[flags] Deprecate is_silent/is_verbose in favor of single flag.Emilio Jesus Gallego Arias
2017-02-14Merge branch 'master'.Pierre-Marie Pédrot
2017-02-14Quick hack to fix interpretation of patterns in Ltac.Pierre-Marie Pédrot
2017-02-14Removing a subtle nf_enter in Class_tactics.Pierre-Marie Pédrot
2017-02-14Chasing a few unsafe constr coercions.Pierre-Marie Pédrot
2017-02-14Definining EConstr-based contexts.Pierre-Marie Pédrot
2017-02-14Evar-normalizing functions now act on EConstrs.Pierre-Marie Pédrot
2017-02-14Removing various compatibility layers of tactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 06:11:42 +0000