index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
Age
Commit message (
Expand
)
Author
2015-06-24
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-06-23
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-01
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-27
Fix bug #4159
Matthieu Sozeau
2015-05-16
Fixing bug #2814: "Anomaly: Uncaught exception Option.IsNone".
Pierre-Marie Pédrot
2015-05-15
Granting wish #4048: Locate Ltac prints the source of redefined Ltac.
Pierre-Marie Pédrot
2015-05-15
Turning "Set Regular Subst Tactic" on by default (for 8.6).
Hugo Herbelin
2015-05-15
Merge v8.5 into trunk
Hugo Herbelin
2015-05-13
Fixing bug #4216:
Pierre-Marie Pédrot
2015-05-13
Safer typing primitives.
Pierre-Marie Pédrot
2015-05-12
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-11
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-09
Adding a flag "Set Regular Subst Tactic" off by default in v8.5 for
Hugo Herbelin
2015-05-06
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-05
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
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-05-04
Code simplification in Tactics.
Pierre-Marie Pédrot
2015-05-01
Giving to "subst" a more natural semantic (fixing #4214) by using all
Hugo Herbelin
2015-04-25
Cleaning some uses of exceptions in tactics.
Pierre-Marie Pédrot
2015-04-23
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-22
Tactical `progress` compares term up to potentially equalisable universes.
Arnaud Spiwack
2015-04-16
Ensuring purity of datastructures in the API.
Pierre-Marie Pédrot
2015-04-15
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-04-14
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-13
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-12
Making the hint entry type opaque.
Pierre-Marie Pédrot
2015-04-10
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-09
Merge branch 'v8.5' into trunk
Pierre Letouzey
2015-04-09
Fix caching of local hintdb in typeclasses eauto.
Matthieu Sozeau
2015-04-06
refresh metas in rewrite hints loaded from .vo files (fix bug #3815)
Nickolai Zeldovich
2015-04-01
Removing a probably incorrect on-the-fly require in a tactic.
Pierre-Marie Pédrot
2015-03-23
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-22
Aliasing give_up with admit
Enrico Tassi
2015-03-11
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-03-11
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
[next]
