aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* Disallow dependent case on prim records w/o etaGravatar Matthieu Sozeau2016-07-06
* primproj: warning and avoid error.Gravatar Matthieu Sozeau2016-07-06
* errors.ml renamed into cErrors.ml (avoid clash with an OCaml compiler-lib mod...Gravatar Pierre Letouzey2016-07-03
* Add and document match, fix and cofix reduction flags.Gravatar Maxime Dénès2016-07-01
* Make semantics of whd_zeta consistent with other whd_* functions.Gravatar Maxime Dénès2016-07-01
* 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
* Shrink Proofs/Obligations by default and deprecateGravatar Matthieu Sozeau2016-06-27
* Typeclasses: fix treatment of exceptions in compatGravatar Matthieu Sozeau2016-06-27
* Typeclasses: mark unresolvable goals in new implementationGravatar Matthieu Sozeau2016-06-27
* We want tclORELSE to catch exceptions on backtrackingsGravatar Matthieu Sozeau2016-06-27
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-27
|\
* | Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optmimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimize the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Optimization in the subst tactic.Gravatar Pierre-Marie Pédrot2016-06-24
* | Small optimization in clear_body.Gravatar Pierre-Marie Pédrot2016-06-20
* | 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
* | A cleaning phase around delayed induction arg + exporting force_induction_arg.Gravatar Hugo Herbelin2016-06-18
* | Adding eintros to respect the e- prefix policy.Gravatar Hugo Herbelin2016-06-18
* | Typeclasses:rename solve_instantiation* & use HookGravatar Matthieu Sozeau2016-06-16
* | Fix resolve_one_typeclass to use the new engineGravatar Matthieu Sozeau2016-06-16
* | Bind resolve_one_typeclass to 8.5 or 8.6 resolutionGravatar Matthieu Sozeau2016-06-16
* | Put autoapply back, lost during rebaseGravatar Matthieu Sozeau2016-06-16
* | Cleanup and refactoringGravatar Matthieu Sozeau2016-06-16
* | Extend Hint Mode to handle the no-head-evar caseGravatar Matthieu Sozeau2016-06-16
* | 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
* | Typeclasses: allow shelved subgoalsGravatar Matthieu Sozeau2016-06-16
* | Minor cleanupGravatar Matthieu Sozeau2016-06-16
* | Typeclasses: refine the eauto tacticGravatar Matthieu Sozeau2016-06-16
* | Typeclasses: verbosity and Limit Intros optionsGravatar Matthieu Sozeau2016-06-16
* | typeclass resolution: add two compatibility optionsGravatar Matthieu Sozeau2016-06-16
* | Fix incorrect caching of local hints w.r.t sectionsGravatar Matthieu Sozeau2016-06-16
* | Compat with ocaml 4.01Gravatar Matthieu Sozeau2016-06-16
* | Fix iterative deepening strategy failing too earlyGravatar 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
* | A stronger invariant on the syntax of TacAssert, what allows for aGravatar Hugo Herbelin2016-06-16
* | Merge 'pr/191' into trunkGravatar Enrico Tassi2016-06-16
|\ \
* \ \ Merge PR #100: fresh now accepts more things than just identifiers.Gravatar Pierre-Marie Pédrot2016-06-16
|\ \ \
| | | * Merge branch 'bug4450' into v8.5Gravatar Matthieu Sozeau2016-06-14
| | | |\
| | * | | Goal selectors are now tacticals and can be used as such.Gravatar Cyprien Mangin2016-06-14
| |/ / / |/| | |
* | | | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-06-13
|\ \ \ \ | | |/ / | |/| |
| * | | Fixing a try with in apply that has become too weak in 8.5.Gravatar Hugo Herbelin2016-06-11