Start documenting new [rewrite_strat] tactic that applies rewriting

according to a given strategy.
- Enhance the hints/lemmas strategy to support "using tac" comming from
rewrite hints to solve side-conditions.  


git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16558 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 7 insertions, 0 deletions

diff --git a/doc/refman/biblio.bib b/doc/refman/biblio.bib
index 192a96998..3715c4c79 100644
--- a/doc/refman/biblio.bib
+++ b/doc/refman/biblio.bib
@@ -786,6 +786,13 @@ of the {ML} language},
   year        = {1990}
 }
 
+@inproceedings{Luttik97specificationof,
+	Author = {Sebastiaan P. Luttik and Eelco Visser},
+	Booktitle = {2nd International Workshop on the Theory and Practice of Algebraic Specifications (ASF+SDF'97), Electronic Workshops in Computing},
+	Publisher = {Springer-Verlag},
+	Title = {Specification of Rewriting Strategies},
+	Year = {1997}}
+
 @Book{MaL84,
   author      = {{P. Martin-L\"of}},
   publisher   = {Bibliopolis},