aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/class_tactics.ml
Commit message (Expand)AuthorAge
* 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
* | | | Removing some return type compatibility layers in Termops.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Reductionops now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Proofview.Goal primitive now return EConstrs.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Eliminating parts of the right-hand side compatibility layerGravatar Pierre-Marie Pédrot2017-02-14
* | | | Class_tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Hints API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Clenv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Tacmach API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Refine API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Goal API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* | | | Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 19:32:48 +0000