aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac/extratactics.ml4
Commit message (Expand)AuthorAge
* 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
|\
| * [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | [coqlib] Move `Coqlib` to `library/`.Gravatar Emilio Jesus Gallego Arias2017-05-27
|/
* Merge branch 'trunk' into located_switchGravatar Emilio Jesus Gallego Arias2017-05-24
|\
| * Fixing grammar for "evar" by exporting the test_lpar_id_colon trick to EXTEND.Gravatar Hugo Herbelin2017-05-16
| * Merge PR#201: Transparent abstractGravatar Maxime Dénès2017-05-11
| |\
| * | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
| * | Remove some unused values and typesGravatar Gaetan Gilbert2017-04-27
| | * Add transparent_abstract tacticGravatar Jason Gross2017-04-25
| |/
* | [location] [ast] Port module AST to CAstGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Make location optional in Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Remove Loc.ghost.Gravatar Emilio Jesus Gallego Arias2017-04-25
* | [location] Switch glob_constr to Loc.locatedGravatar Emilio Jesus Gallego Arias2017-04-24
|/
* Merge branch 'master' into econstrGravatar Pierre-Marie Pédrot2017-04-07
|\
* | Fix a normalization hotspot in computation of constr keys.Gravatar Pierre-Marie Pédrot2017-04-06
* | Using delayed universe instances in EConstr.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
| * Fast path for implicit tactic solving.Gravatar Pierre-Marie Pédrot2017-03-23
|/
* Ltac as a plugin.Gravatar Pierre-Marie Pédrot2017-02-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-25 05:47:34 +0000