aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* 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
* Tauto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Rewrite API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* G_class API using Econstr.Gravatar Pierre-Marie Pédrot2017-02-14
* G_auto API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Extratactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactic_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Eqdecide API using EConstr.Gravatar 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
* Inv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Contradiction API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Equality API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Elim API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tactics API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Hipattern 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
* Making judgment type generic over the type of inner constrs.Gravatar Pierre-Marie Pédrot2017-02-14
* Unification API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Pretyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Cases API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typeclasses API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Tacred API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Constr_matching API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Patternops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Typing API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Evarconv API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Retyping API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Reductionops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Termops API using EConstr.Gravatar Pierre-Marie Pédrot2017-02-14
* Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-29
|\
| * Fixing #5164 (regression in locating error in argument of "refine").Gravatar Hugo Herbelin2016-10-29
* | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-24
|\|
| * Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-22
| * Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
| * Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-10-20
| |\
| | * Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-12
|\| |
| * | Fix bug #5116: [Print Ltac] should be able to print strategies.Gravatar Pierre-Marie Pédrot2016-10-12
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-08
|\| |
| * | Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | | Merge branch 'v8.6'Gravatar Pierre-Marie Pédrot2016-10-02
|\| |
| * | LtacProf cutoff is for total percent, not timeGravatar Jason Gross2016-09-29
| * | Merge branch 'bug5036' into v8.6Gravatar Matthieu Sozeau2016-09-29
| |\ \
| | * | Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-09-29
| | |/
| * / -profile-ltac-cutoff alike Show Ltac Profile Cutoff (#5100)Gravatar Enrico Tassi2016-09-29
| |/
| * Merge remote-tracking branch 'github/pr/232' into v8.6Gravatar Maxime Dénès2016-09-28
| |\
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 19:26:38 +0000