| Commit message (Collapse) | Author | Age |
|---|
| |
|
|
|
| |
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
|
Maxime Dénès
Emilio Jesus Gallego Arias
Guillaume Melquiond
Théo Zimmermann
Enrico Tassi
Hugo Herbelin