| Age | Commit message (Collapse) | Author |
|---|
|
Thanks to Enrico Tassi, Assia Mahboubi, Laurence Rideau and Yves Bertot
for porting this chapter.
|
|
`ssrnat` is mentioned, but it is not distributed with Coq.
|
|
|
|
|
|
The contents should be exactly the same.
I removed the distinction between tactical and pseudo-tactical because
I think that it is too much technical for the introduction. I used
"syntactic construction" and made appeal to the reader intuition
by saying that such construction behaves similarly to a tactical.
I think the text would be much more readable if "the tactics described in
Chapter..." could be replaced by a *name*, but I'm afraid the only
one I could use (Ltac) is a bit too ambiguous. So I'm open to suggestions.
|
|
|
|
|
|
Work done by Assia Mahboubi and Enrico Tassi
|
