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
*
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
|
*
Fix in setoid_rewrite in Type: avoid the generation of a rigid universe
Matthieu Sozeau
2015-12-04
*
|
Removing the last use of valueIn in Tauto.
Pierre-Marie Pédrot
2015-12-04
*
|
Removing dynamic inclusion of constrs in tactic AST.
Pierre-Marie Pédrot
2015-12-04
*
|
Removing the globTacticIn primitive.
Pierre-Marie Pédrot
2015-12-03
*
|
Fixing Tauto compilation for older versions of OCaml.
Pierre-Marie Pédrot
2015-12-03
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
*
|
Removing the last use of tacticIn in setoid_ring.
Pierre-Marie Pédrot
2015-12-03
*
|
Removing the use of tacticIn in Tauto.
Pierre-Marie Pédrot
2015-12-03
|
*
Slight simplification of code for pat/constr.
Hugo Herbelin
2015-12-02
|
*
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
*
|
Removing dead code in Obligations.
Pierre-Marie Pédrot
2015-12-02
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-29
|
\
|
|
*
Fix [Polymorphic Hint Rewrite].
Matthieu Sozeau
2015-11-27
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-26
|
\
|
|
*
Fix generation of equality schemes on polymorphic equality types.
Matthieu Sozeau
2015-11-23
*
|
Removing a use of old refine in Tactics.
Pierre-Marie Pédrot
2015-11-23
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-11-20
|
\
|
|
*
Fix bug #4429: eauto with arith: 70x performance regression in Coq 8.5.
Pierre-Marie Pédrot
2015-11-19
|
*
Fix bug #4433, removing hack on evars appearing in a pattern from a
Matthieu Sozeau
2015-11-19
|
*
Improve error message.
Maxime Dénès
2015-11-18
*
|
Inlining the only use of Clenv.connect_clenv.
Pierre-Marie Pédrot
2015-11-18
[next]