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
*
Fixing incompatibility introduced with simpl in commit 364decf59c1 (or
Hugo Herbelin
2015-06-23
*
With the field record punning syntax.
Theo Zimmermann
2015-06-23
*
Put all arguments of strategy in record.
Theo Zimmermann
2015-06-23
*
Strategy is now a record type with a function field.
Theo Zimmermann
2015-06-23
*
Add comments.
Theo Zimmermann
2015-06-23
*
Fix bug #4159
Matthieu Sozeau
2015-05-27
*
Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".
Pierre-Marie Pédrot
2015-05-16
*
Granting wish #4048: Locate Ltac prints the source of redefined Ltac.
Pierre-Marie Pédrot
2015-05-15
*
Fixing bug #4216:
Pierre-Marie Pédrot
2015-05-13
*
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-13
*
Adding an option Loose Hint Behavior to handle hints loaded but not imported.
Pierre-Marie Pédrot
2015-05-12
*
Adding unique identifiers to hints.
Pierre-Marie Pédrot
2015-05-12
*
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
[next]