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