aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/hints.ml
Commit message (Expand)AuthorAge
* Remove reference name type.Gravatar Maxime Dénès2018-06-18
* Merge PR #7655: Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Pierre-Marie Pédrot2018-06-04
|\
* \ Merge PR #7249: Cleaning, documentation, uniformisation of the Coq extension ...Gravatar Pierre-Marie Pédrot2018-06-04
|\ \
* \ \ Merge PR #7640: Small refactoring to clarify make_local_hint_db.Gravatar Pierre-Marie Pédrot2018-06-04
|\ \ \
| | * | Cleaning, documentation, uniformisation of the Coq extension of List.Gravatar Hugo Herbelin2018-06-03
| |/ / |/| |
* | | Merge PR #7234: Reduce circular dependency constants <-> projectionsGravatar Maxime Dénès2018-06-01
|\ \ \
| | | * Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
| |_|/ |/| |
* | | Merge PR #6969: [api] Remove functions deprecated in 8.8Gravatar Maxime Dénès2018-05-31
|\ \ \
| | * | Reduce circular dependency constants <-> projectionsGravatar Gaëtan Gilbert2018-05-31
* | | | Move interning the [hint_pattern] outside the Typeclasses hooks.Gravatar Gaëtan Gilbert2018-05-30
| |/ / |/| |
| * | [api] Remove deprecated object from `Term`Gravatar Emilio Jesus Gallego Arias2018-05-30
|/ /
* | Merge PR #7558: [api] Make `vernac/` self-contained.Gravatar Maxime Dénès2018-05-30
|\ \
| | * Small refactoring to clarify make_local_hint_db.Gravatar Théo Zimmermann2018-05-30
| |/ |/|
| * [api] Make `vernac/` self-contained.Gravatar Emilio Jesus Gallego Arias2018-05-27
| * [tactics] Turn boolean locality hint parameter into a named one.Gravatar Emilio Jesus Gallego Arias2018-05-27
* | Remove some occurrences of Evd.emptyGravatar Maxime Dénès2018-05-25
|/
* Moving Option.smart_map to Option.Smart.map.Gravatar Hugo Herbelin2018-05-23
* Collecting List.smart_* functions into a module List.Smart.Gravatar Hugo Herbelin2018-05-23
* Split off Universes functions dealing with generating new universes.Gravatar Gaëtan Gilbert2018-05-17
* [api] Rename `global_reference` to `GlobRef.t` to follow kernel style.Gravatar Emilio Jesus Gallego Arias2018-05-04
* [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
* [econstr] Forbid calling `to_constr` in open terms.Gravatar Emilio Jesus Gallego Arias2018-03-31
* [located] Push inner locations in `reference` to a CAst.t node.Gravatar Emilio Jesus Gallego Arias2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* | [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Emilio Jesus Gallego Arias2018-02-28
| * Update headers following #6543.Gravatar Théo Zimmermann2018-02-27
|/
* [proof] Embed evar_map in RefinerError exception.Gravatar Emilio Jesus Gallego Arias2017-12-11
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* [proof] Attempt to deprecate some V82 parts of the proof API.Gravatar Emilio Jesus Gallego Arias2017-11-19
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Better error messages, fix for BZ#5723Gravatar Paul Steckler2017-09-11
* Remove the function Global.type_of_global_unsafe.Gravatar Pierre-Marie Pédrot2017-07-13
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Clean up universes of constants and inductivesGravatar Amin Timany2017-06-16
* [proof] Deprecate redundant wrappers.Gravatar Emilio Jesus Gallego Arias2017-06-11
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Drop '.' from CErrors.anomaly, insert it in argsGravatar Jason Gross2017-06-02
* [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* Merge PR#608: Allow Ltac2 as a pluginGravatar Maxime Dénès2017-05-25
|\
* \ Merge PR#481: [option] Remove support for non-synchronous options.Gravatar Maxime Dénès2017-05-25
|\ \
* \ \ Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\ \ \
| | * | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| |/ /
| | * Allowing to pass arbitrary data in internalization environments.Gravatar Pierre-Marie Pédrot2017-05-03
| |/
| * Remove unused module definition after merging PR#592.Gravatar Maxime Dénès2017-05-02
| * Merge PR#592: Fix bug #5501: Universe polymorphism breaks proof involving auto.Gravatar Maxime Dénès2017-05-02
| |\
| | * Fix bug #5501: Universe polymorphism breaks proof involving auto.Gravatar Pierre-Marie Pédrot2017-04-30
| * | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
| |/
* / [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
|/
* [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\