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
*
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
*
Removing the last quoted auto tactic in Tauto.
Pierre-Marie Pédrot
2015-12-24
*
Finer-grained types for toplevel values.
Pierre-Marie Pédrot
2015-12-21
*
Removing ad-hoc interpretation rules for tactic notations and their genarg.
Pierre-Marie Pédrot
2015-12-21
*
Changing the toplevel type of the int_or_var generic type to int.
Pierre-Marie Pédrot
2015-12-21
*
Removing the now useless genarg generic argument.
Pierre-Marie Pédrot
2015-12-21
*
Using dynamic values in tactic evaluation.
Pierre-Marie Pédrot
2015-12-21
*
Tying the loop in tactic printing API.
Pierre-Marie Pédrot
2015-12-18
*
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-17
|
\
*
|
Getting rid of some hardwired generic arguments.
Pierre-Marie Pédrot
2015-12-17
|
*
FIx parsing of tactic "simple refine".
Maxime Dénès
2015-12-16
|
*
Add a "simple refine" variant of "refine" that does not call "shelve_unifiable".
Guillaume Melquiond
2015-12-16
|
*
Refine tactic now shelves unifiable holes.
Pierre-Marie Pédrot
2015-12-15
|
*
Changing the order of the goals generated by unshelve.
Pierre-Marie Pédrot
2015-12-15
*
|
Granting clear_flag in injection, even legacy mode. This is possible
Hugo Herbelin
2015-12-15
*
|
More code sharing between tactic notation and genarg interpretation.
Pierre-Marie Pédrot
2015-12-13
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
Add tactic native_cast_no_check, analog to vm_cast_no_check.
Maxime Dénès
2015-12-11
|
*
Fixing a pat%constr bug. Thanks to Enrico for reporting.
Hugo Herbelin
2015-12-10
|
*
Silently ignore requests to _not_ clear something when that something cannot ...
Guillaume Melquiond
2015-12-10
|
*
Fixing parsing of the unshelve tactical.
Pierre-Marie Pédrot
2015-12-09
|
*
Adding an unshelve tactical.
Pierre-Marie Pédrot
2015-12-09
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-08
|
\
|
|
*
Fix some typos.
Guillaume Melquiond
2015-12-07
*
|
Fixing compilation with old CAMLPX versions.
Pierre-Marie Pédrot
2015-12-05
*
|
Removing redundant versions of generalize.
Hugo Herbelin
2015-12-05
*
|
Moving extended_rel_vect/extended_rel_list to the kernel.
Hugo Herbelin
2015-12-05
*
|
Experimenting removing strong normalization of the mid-statement in tactic cut.
Hugo Herbelin
2015-12-05
*
|
Moving three related small half-general half-ad-hoc utility functions
Hugo Herbelin
2015-12-05
*
|
Getting rid of some quoted tactics in Tauto.
Pierre-Marie Pédrot
2015-12-05
*
|
Getting rid of the dynamic node of the tactic AST.
Pierre-Marie Pédrot
2015-12-04
[next]