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
*
Adding a test to check whether two tactic notations conflict.
Pierre-Marie Pédrot
2015-05-11
*
Fixing bug #4232.
Pierre-Marie Pédrot
2015-05-11
*
Rationalizing a bit the interface of Hints.
Pierre-Marie Pédrot
2015-05-11
*
Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for
Hugo Herbelin
2015-05-09
*
Fixing treatment of recursive equations damaged by 857e82b2ca0d1.
Hugo Herbelin
2015-05-06
*
Fixing "subst" to respect v8.4 most-ancient to most-recent hyps order
Hugo Herbelin
2015-05-06
*
Removing dead code in Rewrite.
Pierre-Marie Pédrot
2015-05-05
*
Making the strategy type in Rewrite opaque.
Pierre-Marie Pédrot
2015-05-05
*
Code simplification in Tactics.
Pierre-Marie Pédrot
2015-05-04
*
Giving to "subst" a more natural semantic (fixing #4214) by using all
Hugo Herbelin
2015-05-01
*
Cleaning some uses of exceptions in tactics.
Pierre-Marie Pédrot
2015-04-25
*
Remove almost all the uses of string concatenation when building error messages.
Guillaume Melquiond
2015-04-23
*
Using tclZEROMSG instead of tclZERO in several places.
Pierre-Marie Pédrot
2015-04-23
*
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-22
*
Ensuring purity of datastructures in the API.
Pierre-Marie Pédrot
2015-04-16
*
Cleaning up the implementation of search entries in Hints.
Pierre-Marie Pédrot
2015-04-14
*
Opaque implementation of auto tactics.
Pierre-Marie Pédrot
2015-04-14
*
Remove declarations of matched variables in change as an extension of
Matthieu Sozeau
2015-04-13
*
More documented representation of hint objects.
Pierre-Marie Pédrot
2015-04-13
*
Making the hint entry type opaque.
Pierre-Marie Pédrot
2015-04-12
*
Fix compilation broken by Matthieu's last commit.
Pierre Letouzey
2015-04-10
*
Fix #3590 for good this time, by changing the API, change's argument now
Matthieu Sozeau
2015-04-10
*
Eauto hints respect their priority. Fixes bug #3199.
Pierre-Marie Pédrot
2015-04-10
*
Making the hints for the auto tactics private.
Pierre-Marie Pédrot
2015-04-10
*
Fix caching of local hintdb in typeclasses eauto.
Matthieu Sozeau
2015-04-09
*
refresh metas in rewrite hints loaded from .vo files (fix bug #3815)
Nickolai Zeldovich
2015-04-06
*
Removing a probably incorrect on-the-fly require in a tactic.
Pierre-Marie Pédrot
2015-04-01
*
Aliasing give_up with admit
Enrico Tassi
2015-03-22
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Reverting r10021 which enforces early assumptions on freshness which
Hugo Herbelin
2015-03-07
*
Continuing a8ad3abc15a2 and 60810aaec on freshness of name in tactic "evar".
Hugo Herbelin
2015-03-07
*
Fix bug #3590, keeping evars that are not turned into named metas by
Matthieu Sozeau
2015-03-03
*
Removing the unused field ltacrecvars of tactic internalization.
Pierre-Marie Pédrot
2015-02-27
*
Hack so that refine_no_check accepts an argument which is a match on an
Hugo Herbelin
2015-02-27
*
Somehow fixing bug #3467.
Pierre-Marie Pédrot
2015-02-27
*
Fixing bug #3298.
Pierre-Marie Pédrot
2015-02-26
*
Fixing printing of ordinals.
Pierre-Marie Pédrot
2015-02-26
*
[info_auto] & [info_trivial]: warning message to help users find [Info].
Arnaud Spiwack
2015-02-24
*
[info] tactical warning: do not suggest [info_auto] and [info_trivial].
Arnaud Spiwack
2015-02-24
*
Fix some typos in comments.
Guillaume Melquiond
2015-02-23
*
Fixing error message when H already exists in tactic subexpression eqn:H.
Hugo Herbelin
2015-02-20
*
A fix for #3993 (not fully applied term to destruct when eqn is given).
Hugo Herbelin
2015-02-20
*
Fix bug #3938
Matthieu Sozeau
2015-02-18
*
Fixing bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Fixing bug #4016.
Pierre-Marie Pédrot
2015-02-14
*
Univs: fix bug #4031: wrong folding of sigma in change.
Matthieu Sozeau
2015-02-12
*
Fix bug #2775: Correct handling of universes in leminv.
Matthieu Sozeau
2015-02-12
*
Fixing compilation for 3.12.
Pierre-Marie Pédrot
2015-02-12
*
Tentative fix for bug #4027.
Pierre-Marie Pédrot
2015-02-12
*
Missing space in error message
Matěj Grabovský
2015-02-11
[next]