aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/extratactics.ml4
Commit message (Expand)AuthorAge
* Change QuestionMark for better record field missing error message.Gravatar Siddharth Bhat2018-07-17
* refine: obey the use_unification_heuristics flagGravatar Matthieu Sozeau2018-07-05
* Fix #7421: constr_eq ignores universe constraints.Gravatar Gaëtan Gilbert2018-06-18
* [api] Misctypes removal: several moves:Gravatar Emilio Jesus Gallego Arias2018-06-12
* Merge PR #7229: Deprecate implicit tactic solving.Gravatar Hugo Herbelin2018-06-04
|\
| * Deprecate implicit tactic solving.Gravatar Pierre-Marie Pédrot2018-06-04
* | Refactor parsing rules for Hint Resolve -> and Hint Resolve <-Gravatar Armaël Guéneau2018-05-31
|/
* [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
|\
| * [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
|/
* [api] Move `hint_info_expr` to `Typeclasses`.Gravatar Emilio Jesus Gallego Arias2018-04-26
* Evar maps contain econstrs.Gravatar Gaëtan Gilbert2018-04-13
* [located] More work towards using CAst.tGravatar Emilio Jesus Gallego Arias2018-03-09
* Allow using cumulativity without forcing strict constraints.Gravatar Gaëtan Gilbert2018-03-09
* Merge PR #6855: Update headers following #6543.Gravatar Maxime Dénès2018-03-05
|\
* \ Merge PR #6511: [econstr] Continue consolidation of EConstr API under `interp`.Gravatar Maxime Dénès2018-03-04
|\ \
* \ \ Merge PR #6676: [proofview] goals come with a stateGravatar Maxime Dénès2018-03-04
|\ \ \
| | * | [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
| |/ |/|
* | [ast] Improve precision of Ast location recognition in serialization.Gravatar Emilio Jesus Gallego Arias2018-02-22
| * proofview: goals come with a stateGravatar Enrico Tassi2018-02-20
|/
* Change references to CAMLP4 to CAMLP5 to be more accurate since we noGravatar Jim Fehrle2018-02-17
* Merge PR #6497: Add optimize_heap tactic for #6488Gravatar Maxime Dénès2018-01-08
|\
| * add optimize_heap tactic for #6488Gravatar Paul Steckler2018-01-03
* | Remove the local polymorphic flag hack.Gravatar Maxime Dénès2017-12-27
|/
* Merge PR #1033: Universe binder improvementsGravatar Maxime Dénès2017-11-28
|\
* | Use Evarutil.has_undefined_evars for tactic has_evar.Gravatar Gaëtan Gilbert2017-11-24
| * Use Entries.constant_universes_entry more.Gravatar Gaëtan Gilbert2017-11-24
|/
* Merge PR #6197: [plugin] Remove LocalityFixme über hack.Gravatar Maxime Dénès2017-11-24
|\
| * [plugin] Remove LocalityFixme über hack.Gravatar Emilio Jesus Gallego Arias2017-11-22
* | Fix #5790: make Hint Resolve <- respect univ polymorphism flag.Gravatar Gaëtan Gilbert2017-11-19
|/
* [api] Move structures deprecated in the API to the core.Gravatar Emilio Jesus Gallego Arias2017-11-06
* Passing around the flag for injection so that tactics calling inj atGravatar Hugo Herbelin2017-10-26
* Efficient fresh name generation relying on sets.Gravatar Pierre-Marie Pédrot2017-09-28
* Parse directly to Sorts.family when appropriate.Gravatar Gaëtan Gilbert2017-09-08
* Making detyping potentially lazy.Gravatar Pierre-Marie Pédrot2017-09-04
* Move type_uconstr to Tacinterp.Gravatar Maxime Dénès2017-08-01
* [api] Remove type equalities from API.Gravatar Emilio Jesus Gallego Arias2017-07-25
* [API] Remove `open API` in ml files in favor of `-open API` flag.Gravatar Emilio Jesus Gallego Arias2017-07-17
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* plugins/ltac : avoid spurious .cmxs filesGravatar Pierre Letouzey2017-06-15
* Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
* Remove (useless) aliases from the API.Gravatar Matej Košík2017-06-10
* Put all plugins behind an "API".Gravatar Matej Kosik2017-06-07
* Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* Merge PR#696: Trunk+cleanup constr of globalGravatar Maxime Dénès2017-06-01
|\
* | Support for using type information to infer more precise evar sources.Gravatar Hugo Herbelin2017-05-30
| * Ltac cleanup: no more constr_of_global callsGravatar Matthieu Sozeau2017-05-29
|/
* Merge PR#512: [cleanup] Unify all calls to the error function.Gravatar Maxime Dénès2017-05-29
|\
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-10 07:51:23 +0000