aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac
Commit message (Expand)AuthorAge
* 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
* Separate flags for fix/cofix/match reduction and clean reduction function names.Gravatar Maxime Dénès2016-07-01
* A new infrastructure for warnings.Gravatar Maxime Dénès2016-06-29
* LtacProf reports structured results (pr/209)Gravatar CJ Bell2016-06-20
* Do not evar-normalize goals when interpreting some hardwired genargs.Gravatar Pierre-Marie Pédrot2016-06-20
* Backporting c064fb933 from 8.5 (another regression with Ltac trace report).Gravatar Hugo Herbelin2016-06-18
* Adding an "as" clause to specialize.Gravatar Hugo Herbelin2016-06-18
* Giving a more natural semantics to injection by default.Gravatar Hugo Herbelin2016-06-18
* Exporting a generic argument induction_arg. As a consequence,Gravatar Hugo Herbelin2016-06-18
* Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* par: like all: but in parallelGravatar Enrico Tassi2016-06-17
* Revise syntax of Hint CutGravatar Matthieu Sozeau2016-06-16
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* bteauto: a Proofview.tactic for multiple goalsGravatar Matthieu Sozeau2016-06-16
* Implement limited proof search and iterative deepening.Gravatar Matthieu Sozeau2016-06-16
* Typeclasses eauto based on new proof engine,Gravatar Matthieu Sozeau2016-06-16
* Typo in comment.Gravatar Hugo Herbelin2016-06-16
* Fixing space in an error message.Gravatar Hugo Herbelin2016-06-16
* Fixing printing of Register retroknowledge.Gravatar Hugo Herbelin2016-06-16
* Fixing Add Parametric Relation by adding printer for binders.Gravatar Hugo Herbelin2016-06-16
* Fixing missing substitution / printing cases of TacSelect.Gravatar Pierre-Marie Pédrot2016-06-16
* Fixing parsing of constr argument of ltac functions at level 8 in theGravatar Hugo Herbelin2016-06-16
* A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* Merge PR #195: Complete is_* family of term-examining tactics.Gravatar Pierre-Marie Pédrot2016-06-16
|\
* \ Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* \ \ Merge PR #211: Fix a printing typo in LtacProf.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-01 06:01:28 +0000