aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics
Commit message (Expand)AuthorAge
* CLEANUP: Context.{Rel,Named}.Declaration.tGravatar Matej Kosik2016-02-09
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-29
|\
| * Fix bug #4537: Coq 8.5 is slower in typeclass resolution.Gravatar Pierre-Marie Pédrot2016-01-27
| * Fixing bug #4511: evar tactic can create non-typed evars.Gravatar Pierre-Marie Pédrot2016-01-24
| * Implement support for universe binder lists in Instance and Program Fixpoint/...Gravatar Matthieu Sozeau2016-01-23
* | Fixing a use of "clear" on an non-existing hypothesis in intro-patterns.Gravatar Hugo Herbelin2016-01-22
* | New step on recent 9c2662eecc398f3 (strong invariants on tuple pattern).Gravatar Hugo Herbelin2016-01-21
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-21
|\|
* | Stronger invariants on the use of the introduction pattern (pat1,...,patn).Gravatar Hugo Herbelin2016-01-21
* | Fixing some problems with double induction.Gravatar Hugo Herbelin2016-01-21
* | Code simplification in elim.ml.Gravatar Hugo Herbelin2016-01-20
* | Fixing a bug with introduction patterns over inductive types containing let-ins.Gravatar Hugo Herbelin2016-02-18
| * Update copyright headers.Gravatar Maxime Dénès2016-01-20
| * Fix bug #4420: check_types was losing universe constraints.Gravatar Matthieu Sozeau2016-01-19
* | Moving val_cast to Tacinterp.Gravatar Pierre-Marie Pédrot2016-01-17
* | Getting rid of the awkward unpack mechanism from Genarg.Gravatar Pierre-Marie Pédrot2016-01-17
* | Removing constr generic argument.Gravatar Pierre-Marie Pédrot2016-01-14
* | Removing ident and var generic arguments.Gravatar Pierre-Marie Pédrot2016-01-14
* | Moving is_quantified_hypothesis to new proof engine.Gravatar Hugo Herbelin2016-01-14
* | Update in the documentation of parts of the code of destruct/induction.Gravatar Hugo Herbelin2016-01-14
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-01-13
|\|
| * Fix essential bug in new Keyed Unification mode reported by R. Krebbers.Gravatar Matthieu Sozeau2016-01-12
* | CLEANUP: removing unused fieldGravatar Matej Kosik2016-01-11
* | mergeGravatar Matej Kosik2016-01-11
|\ \
| * | CLEANUP: kernel/context.ml{,i}Gravatar Matej Kosik2016-01-11
| | * Fix bug #3338 again, no progress is necessary for the success of rewrite_strat.Gravatar Matthieu Sozeau2016-01-11
* | | Fix bug 4479: "Error: Rewriting base foo does not exist." should be catchable.Gravatar Pierre-Marie Pédrot2016-01-09
* | | Monotonizing Ftactic.Gravatar Pierre-Marie Pédrot2016-01-08
| | * Fix bug #4480: progress was not checked for setoid_rewrite.Gravatar Matthieu Sozeau2016-01-07
* | | Remove some unused functions.Gravatar Guillaume Melquiond2016-01-02
* | | Remove duplicate definition.Gravatar Guillaume Melquiond2016-01-02
* | | Remove duplicate declarations.Gravatar Guillaume Melquiond2016-01-02
* | | Reduce dependencies of interface files.Gravatar Guillaume Melquiond2016-01-02
* | | Remove useless rec flags.Gravatar Guillaume Melquiond2016-01-02
* | | Separation of concern in TacAlias API.Gravatar Pierre-Marie Pédrot2016-01-02
* | | Moving apply_type to new proof engine.Gravatar Hugo Herbelin2015-12-30
* | | Taking into account generated typing constraints in tactic "generalize".Gravatar Hugo Herbelin2015-12-30
* | | External tactics and notations now accept any tactic argument.Gravatar Pierre-Marie Pédrot2015-12-30
* | | Implementing non-focussed generic arguments.Gravatar Pierre-Marie Pédrot2015-12-28
* | | Removing the special status of open_constr generic argument.Gravatar Pierre-Marie Pédrot2015-12-28
* | | Eradicating uses of open_constr in TACTIC EXTEND in favour of uconstr.Gravatar Pierre-Marie Pédrot2015-12-28
* | | Factorizing code for untyped constr evaluation.Gravatar Pierre-Marie Pédrot2015-12-27
* | | Removing dead code.Gravatar Pierre-Marie Pédrot2015-12-27
* | | Tentative API fix for tactic arguments to be fed to tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-12-27
* | | Moving basic generalization tactics upwards for possible use in "intros".Gravatar Hugo Herbelin2015-12-25
* | | Moving code of specialize so that it can accept "as" (no semantic change).Gravatar Hugo Herbelin2015-12-25
* | | Moving specialize to Proofview.tactic.Gravatar Hugo Herbelin2015-12-25
* | | Fixing a bug in the order of side conditions for introduction pattern -> and <-.Gravatar Hugo Herbelin2015-12-25
* | | Fixing an "injection as" bug in the presence of side conditions.Gravatar Hugo Herbelin2015-12-25
* | | Moving the ad hoc interpretation of "intros" as "intros **" from tacinterp.mlGravatar Hugo Herbelin2015-12-25
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-02 20:58:53 +0000