aboutsummaryrefslogtreecommitdiffhomepage
path: root/ltac/extratactics.ml4
Commit message (Expand)AuthorAge
* 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
* | More explicit name for status of unification constraints.Gravatar Maxime Dénès2016-11-07
| * Fix handling of only_classes at toplevelGravatar Matthieu Sozeau2016-11-03
| * Lets Hints/Instances take an optional patternGravatar Matthieu Sozeau2016-11-03
* | Unification constraint handling (#4763, #5149)Gravatar Matthieu Sozeau2016-10-22
|/
* Revert 214b9ab7969fae71dcf553c399cb1674e463d0e3Gravatar Matthieu Sozeau2016-10-21
* Fix bug #5036 autorewrite, sections and universesGravatar Matthieu Sozeau2016-10-20
* Fix bug #4893: not_evar: unexpected failure in 8.5pl1.Gravatar Pierre-Marie Pédrot2016-08-30
* Merge branch 'v8.5' into trunkGravatar Maxime Dénès2016-07-04
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* 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
* Purely refactoring and code/API cleanup.Gravatar Matthieu Sozeau2016-06-16
* Merge PR #195: Complete is_* family of term-examining tactics.Gravatar Pierre-Marie Pédrot2016-06-16
|\
| * Add is_constGravatar Jason Gross2016-06-16
| * Add is_ind, is_constructor, is_projGravatar Jason Gross2016-06-07
* | STM: proof block detection/error resilience APIGravatar Enrico Tassi2016-06-06
|/
* Feedback cleanupGravatar Emilio Jesus Gallego Arias2016-05-31
* Put the "specialize_eq" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Put the "generalize" tactic in the monad.Gravatar Pierre-Marie Pédrot2016-05-16
* Removing dead code and unused opens.Gravatar Pierre-Marie Pédrot2016-05-08
* Removing useless generic arguments.Gravatar Pierre-Marie Pédrot2016-05-04
* More toplevel value representation sharing.Gravatar Pierre-Marie Pédrot2016-05-04
* Moving the Val module to Geninterp.Gravatar Pierre-Marie Pédrot2016-05-04
* Removing redundant *_TYPED AS clauses in EXTEND statements.Gravatar Pierre-Marie Pédrot2016-04-12
* Making Autorewrite independent from Ltac.Gravatar Pierre-Marie Pédrot2016-03-25
* Moving type_uconstr to Pretyping.Gravatar Pierre-Marie Pédrot2016-03-25
* Creating a dedicated ltac/ folder for Hightactics.Gravatar Pierre-Marie Pédrot2016-03-21
generated by cgit v1.2.3 (git 2.39.1) at 2024-12-05 01:55:32 +0000