aboutsummaryrefslogtreecommitdiff
path: root/ltac/extratactics.ml4
AgeCommit message (Expand)Author
2017-02-17Ltac as a plugin.Pierre-Marie Pédrot
2016-11-22Fix locality of "Hint Resolve <->" (bug #5189).Guillaume Melquiond
2016-11-18Merge branch 'v8.6'Pierre-Marie Pédrot
2016-11-07Merge remote-tracking branch 'github/pr/339' into v8.6Maxime Dénès
2016-11-07Fixes to compile with ocaml 4.01Matthieu Sozeau
2016-11-07More explicit name for status of unification constraints.Maxime Dénès
2016-11-03Fix handling of only_classes at toplevelMatthieu Sozeau
2016-11-03Lets Hints/Instances take an optional patternMatthieu Sozeau
2016-10-24Merge branch 'v8.6'Pierre-Marie Pédrot
2016-10-22Unification constraint handling (#4763, #5149)Matthieu Sozeau
2016-10-21Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Matthieu Sozeau
2016-10-20Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
2016-10-02Merge branch 'v8.6'Pierre-Marie Pédrot
2016-09-29Fix bug #5036 autorewrite, sections and universesMatthieu Sozeau
2016-09-21Merging Stdarg and Constrarg.Pierre-Marie Pédrot
2016-09-15Moving Ltac-specific generic arguments to their own file in the ltac/ folder.Pierre-Marie Pédrot
2016-09-14Moving Ltac-specific parsing API to ltac/ folder.Pierre-Marie Pédrot
2016-09-08Unplugging Pptactic from Ppvernac.Pierre-Marie Pédrot
2016-08-30Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Pierre-Marie Pédrot
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-02-11 08:52:55 +0000