aboutsummaryrefslogtreecommitdiff
path: root/ltac
AgeCommit message (Expand)Author
2016-06-16Revise syntax of Hint CutMatthieu Sozeau
2016-06-16Purely refactoring and code/API cleanup.Matthieu Sozeau
2016-06-16bteauto: a Proofview.tactic for multiple goalsMatthieu Sozeau
2016-06-16Implement limited proof search and iterative deepening.Matthieu Sozeau
2016-06-16Typeclasses eauto based on new proof engine,Matthieu Sozeau
2016-06-16Typo in comment.Hugo Herbelin
2016-06-16Fixing space in an error message.Hugo Herbelin
2016-06-16Fixing printing of Register retroknowledge.Hugo Herbelin
2016-06-16Fixing Add Parametric Relation by adding printer for binders.Hugo Herbelin
2016-06-16Fixing missing substitution / printing cases of TacSelect.Pierre-Marie Pédrot
2016-06-16Fixing parsing of constr argument of ltac functions at level 8 in theHugo Herbelin
2016-06-16A stronger invariant on the syntax of TacAssert, what allows for aHugo Herbelin
2016-06-16Merge PR #195: Complete is_* family of term-examining tactics.Pierre-Marie Pédrot
2016-06-16Merge 'pr/191' into trunkEnrico Tassi
2016-06-16Merge PR #211: Fix a printing typo in LtacProf.Pierre-Marie Pédrot
2016-06-16Merge PR #100: fresh now accepts more things than just identifiers.Pierre-Marie Pédrot
2016-06-16Add is_constJason Gross
2016-06-16Fix another missing newlineJason Gross
2016-06-16Fix a printing typoJason Gross
2016-06-14Merge remote-tracking branch 'origin/pr/173' into trunkEnrico Tassi
2016-06-14Ident selectors cannot be used inside an Ltac expression.Cyprien Mangin
2016-06-14Goal selectors are now tacticals and can be used as such.Cyprien Mangin
2016-06-14Remove the need for brackets in goal selectors.Cyprien Mangin
2016-06-14Fix usage of Pervasives in goal selectors.Cyprien Mangin
2016-06-14Fix the pretty-printing of goal range selectors.Cyprien Mangin
2016-06-14Add goal range selectors.Cyprien Mangin
2016-06-14Merge branch "LtacProf for trunk" (PR #165).Pierre-Marie Pédrot
2016-06-14Commenting out debugging code.Pierre-Marie Pédrot
2016-06-14Correct use of printing primitives.Pierre-Marie Pédrot
2016-06-14Better coding style (semantics).Pierre-Marie Pédrot
2016-06-14Better coding style (syntax).Pierre-Marie Pédrot
2016-06-14Adding Coq headers.Pierre-Marie Pédrot
2016-06-14Moving back Ltac profiling to the Ltac folder.Pierre-Marie Pédrot
2016-06-13Revert "Strip some trailing spaces"Pierre-Marie Pédrot
2016-06-09Merge branch 'v8.5'Pierre-Marie Pédrot
2016-06-07Add is_ind, is_constructor, is_projJason Gross
2016-06-06About printing of traces of failures while calling ltac code.Hugo Herbelin
2016-06-06STM: proof block detection for par:Enrico Tassi
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-06-05Make Ltac Profiling an settingJason Gross
2016-06-05Synchronize the profiler state with the documentJason Gross
2016-06-05LtacProf for Coq trunkJason Gross
2016-06-05Strip some trailing spacesJason Gross
2016-06-05Adding the Print Ltac Signature command.Pierre-Marie Pédrot
2016-06-03Removing "rename" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "exact" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "intro" from the tactic AST.Pierre-Marie Pédrot
2016-06-03Removing "double induction" from the tactic AST.Pierre-Marie Pédrot
2016-06-02Add a synonymous Set Debug Ltac for Set Ltac Debug, for uniformity.Hugo Herbelin
2016-06-01Merge branch 'v8.5'Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 06:07:11 +0000