aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
Commit message (Expand)AuthorAge
* [printing] Deprecate all printing functions accessing the global proof.Gravatar Emilio Jesus Gallego Arias2017-11-21
* Merge PR #805: Functional tacticsGravatar Maxime Dénès2017-08-29
|\
* \ Merge PR #919: Remove a few useless evar-normalizations in printing code.Gravatar Maxime Dénès2017-08-01
|\ \
* \ \ Merge PR #761: deprecate Pp.std_ppcmds type and promote Pp.t insteadGravatar Maxime Dénès2017-07-31
|\ \ \
| | | * env, sigma as first arguments of functionsGravatar amblaf2017-07-31
| | | * Remove references to Global.env in tactics/*.mlGravatar amblaf2017-07-31
| |_|/ |/| |
| * | deprecate Pp.std_ppcmds type aliasGravatar Matej Košík2017-07-27
| | * Remove a few useless evar-normalizations in printing code.Gravatar Pierre-Marie Pédrot2017-07-26
| |/ |/|
* | Merge PR #868: Fix debug trace of typeclasses eauto.Gravatar Maxime Dénès2017-07-26
|\ \ | |/ |/|
* | Merge PR #892: Improve do_split option of typeclass resolutionGravatar Maxime Dénès2017-07-20
|\ \
* \ \ Merge PR #869: Enforce alternating separators in typeclass debug outputGravatar Maxime Dénès2017-07-20
|\ \ \
| | | * Fix debug trace of typeclasses eauto.Gravatar Théo Zimmermann2017-07-19
| | * | Improve do_split option of typeclass resolutionGravatar Matthieu Sozeau2017-07-18
| | |/
| * / format pairs of items for pr_depth to get alternating separatorsGravatar Paul Steckler2017-07-12
| |/
* / Deprecate options that were introduced for compatibility with 8.5.Gravatar Théo Zimmermann2017-07-11
|/
* Bump year in headers.Gravatar Pierre-Marie Pédrot2017-07-04
* Merge PR#787: [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Maxime Dénès2017-06-19
|\
* \ Merge PR#727: [tactics] Fix summary registration of global hint variable.Gravatar Maxime Dénès2017-06-19
|\ \
| | * [typeclasses eauto] Fix bug #3943: non-termination in topologicalGravatar Matthieu Sozeau2017-06-14
* | | Dualize the unsafe flag of refine into typecheck and make it mandatory.Gravatar Pierre-Marie Pédrot2017-06-13
| |/ |/|
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-06-08
|\ \
* | | Remove the Sigma (monotonous state) API.Gravatar Maxime Dénès2017-06-06
* | | Merge PR#638: Fix bug #5360: anomalies in typeclass resolution outputGravatar Maxime Dénès2017-06-06
|\ \ \
| | | * [tactics] Fix summary registration of global hint variable.Gravatar Emilio Jesus Gallego Arias2017-06-03
| |_|/ |/| |
| | * Fix bug 5550: "typeclasses eauto with" does not work with section variables.Gravatar Théo Zimmermann2017-05-30
* | | [cleanup] Unify all calls to the error function.Gravatar Emilio Jesus Gallego Arias2017-05-27
* | | [option] Remove support for non-synchronous options.Gravatar Emilio Jesus Gallego Arias2017-05-24
| * | Fix bug #5360: anomalies in typeclass resolution outputGravatar Matthieu Sozeau2017-05-16
* | | Uniformity of style for selecting plural or not; spacing for comma.Gravatar Hugo Herbelin2017-05-13
|/ /
* | Post-rebase warnings (unused opens and 2 unused values)Gravatar Gaetan Gilbert2017-04-27
* | Remove unused [open] statementsGravatar Gaetan Gilbert2017-04-27
* | Fix omitted labels in function callsGravatar Gaetan Gilbert2017-04-27
* | Removing various tactic compatibility layers in core tactics.Gravatar Pierre-Marie Pédrot2017-04-24
* | Removing the tclWEAK_PROGRESS tactical.Gravatar Pierre-Marie Pédrot2017-04-24
* | [flags] Deprecate is_silent/is_verbose in favor of single flag.Gravatar Emilio Jesus Gallego Arias2017-04-21
* | Fix a heuristic used by legacy typeclass resolution.Gravatar Pierre-Marie Pédrot2017-04-08
* | Actually exporting delayed universes in the EConstr implementation.Gravatar Pierre-Marie Pédrot2017-04-01
* | Merge branch 'trunk' into pr379Gravatar Maxime Dénès2017-03-24
|\ \
| * | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2017-03-22
| |\|
| | * Merge PR#359: Fix bug 4969, autoapply was not tagging shelved subgoals correc...Gravatar Maxime Dénès2017-03-10
| | |\
* | | | Merge branch 'master'.Gravatar Pierre-Marie Pédrot2017-02-14
|\| | |
* | | | Removing a subtle nf_enter in Class_tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing most nf_enter in tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Namegen primitives now apply on evar constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Definining EConstr-based contexts.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Introducing contexts parameterized by the inner term type.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Evar-normalizing functions now act on EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing various compatibility layers of tactics.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing compatibility layers related to printing.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Removing compatibility layers in RetypingGravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-14 11:19:37 +0000