aboutsummaryrefslogtreecommitdiff
path: root/ltac/extratactics.ml4
AgeCommit message (Expand)Author
2016-07-04Merge branch 'v8.5' into trunkMaxime Dénès
2016-07-03errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Pierre Letouzey
2016-06-18Giving a more natural semantics to injection by default.Hugo Herbelin
2016-06-18Exporting a generic argument induction_arg. As a consequence,Hugo Herbelin
2016-06-18Adding eintros to respect the e- prefix policy.Hugo Herbelin
2016-06-16Purely refactoring and code/API cleanup.Matthieu Sozeau
2016-06-16Merge PR #195: Complete is_* family of term-examining tactics.Pierre-Marie Pédrot
2016-06-16Add is_constJason Gross
2016-06-07Add is_ind, is_constructor, is_projJason Gross
2016-06-06STM: proof block detection/error resilience APIEnrico Tassi
2016-05-31Feedback cleanupEmilio Jesus Gallego Arias
2016-05-16Put the "specialize_eq" tactic in the monad.Pierre-Marie Pédrot
2016-05-16Put the "generalize" tactic in the monad.Pierre-Marie Pédrot
2016-05-08Removing dead code and unused opens.Pierre-Marie Pédrot
2016-05-04Removing useless generic arguments.Pierre-Marie Pédrot
2016-05-04More toplevel value representation sharing.Pierre-Marie Pédrot
2016-05-04Moving the Val module to Geninterp.Pierre-Marie Pédrot
2016-04-12Removing redundant *_TYPED AS clauses in EXTEND statements.Pierre-Marie Pédrot
2016-03-25Making Autorewrite independent from Ltac.Pierre-Marie Pédrot
2016-03-25Moving type_uconstr to Pretyping.Pierre-Marie Pédrot
2016-03-21Creating a dedicated ltac/ folder for Hightactics.Pierre-Marie Pédrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-21 01:06:58 +0000