aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* Fixing printers for pr_auto_using and pr_firstorder_using.Gravatar Hugo Herbelin2016-12-02
* Fix bug #5232: proper globalization of hints pathsGravatar Matthieu Sozeau2016-11-30
* Merge remote-tracking branch 'github/pr/339' into v8.6Gravatar Maxime Dénès2016-11-07
|\
| * Fixes to compile with ocaml 4.01Gravatar Matthieu Sozeau2016-11-07
* | Merge commit 'e6edb33' into v8.6Gravatar Maxime Dénès2016-11-07
|\ \
| * | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| | * Rework search_strategy option handlingGravatar Matthieu Sozeau2016-11-03
| | * Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
| | * Fix Typeclasses eauto := bfs.Gravatar Matthieu Sozeau2016-11-03
| | * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
| |/ |/|
* | Fixing #5164 (regression in locating error in argument of "refine").Gravatar Hugo Herbelin2016-10-29
* | Merge branch 'v8.5' into v8.6Gravatar Hugo Herbelin2016-10-22
| * Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-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
* | Fix bug #5116: [Print Ltac] should be able to print strategies.Gravatar Pierre-Marie Pédrot2016-10-12
* | Fix bug #5098: Symmetry broken in HoTT.Gravatar Pierre-Marie Pédrot2016-10-08
* | 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
|\
* | LtacProf: "Show Ltac Profile CutOff $N" (fix #5080)Gravatar Enrico Tassi2016-09-27
* | Fix bug #5093: typeclasses eauto depth arg does not accept a var.Gravatar Pierre-Marie Pédrot2016-09-26
* | Continuing fix to #5078, taking also into account intropatterns.Gravatar Hugo Herbelin2016-09-15
* | Fixing #5078 (wrong detection of evaluable local hypotheses).Gravatar Hugo Herbelin2016-09-13
* | LtacProp: fix reset_profile (fix #5079)Gravatar Enrico Tassi2016-09-13
* | Fix newlines in printout of LtacProfGravatar Jason Gross2016-09-11
* | Revert the LtacProf tactic table headerGravatar Jason Gross2016-09-11
* | Fix bug #3920 for good after 44ada64.Gravatar Pierre-Marie Pédrot2016-09-09
* | Removing useless tactic compatibility layer in Rewrite.Gravatar Pierre-Marie Pédrot2016-09-07
* | ltacprof: rec-calls are coaleshedGravatar Enrico Tassi2016-09-07
* | profile_ltac: rewritten to be purely functional and STM awareGravatar Enrico Tassi2016-09-05
* | Moving log of "TacReduce"/"reduce" to Tactics.reduce so that internalGravatar Hugo Herbelin2016-09-01
* | Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-08-30
* | Fix bug #3920: eapply masks an hypothesis name.Gravatar Pierre-Marie Pédrot2016-08-30
* | Fix bug #4914: LtacProf printout has too many newlines.Gravatar Pierre-Marie Pédrot2016-08-23
* | Moving Taccoerce to ltac/ folder.Gravatar Pierre-Marie Pédrot2016-08-19
* | Merge remote-tracking branch 'github/bug4188' into v8.6Gravatar Matthieu Sozeau2016-08-18
|\ \
* | | Fix bug #4939: LtacProf prints tactic notations weirdly.Gravatar Pierre-Marie Pédrot2016-08-18
| * | Fix setoid_rewrite to raise proper errorsGravatar Matthieu Sozeau2016-08-17
|/ /
* | Merge branch 'v8.5' into v8.6Gravatar Pierre-Marie Pédrot2016-08-16
* | Merge remote-tracking branch 'gforge/v8.5' into v8.6Gravatar Matthieu Sozeau2016-07-29
* | Fix bug #4679, weakened setoid_rewrite unificationGravatar Matthieu Sozeau2016-07-21
* | Revert "Revert "Improve the interpretation scope of arguments of an ltac matc...Gravatar Maxime Dénès2016-07-04
* | Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
* | rename toplevel/cerror.ml into explainErr.ml (too close to the new lib/cError...Gravatar Pierre Letouzey2016-07-03
* | closure.ml renamed into cClosure.ml (avoid clash with a compiler-libs module)Gravatar Pierre Letouzey2016-07-03
* | errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03