| Age | Commit message (Collapse) | Author |
|---|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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
|
|
The term of type `list nat` should be `(@nil nat)` instead of `(nil nat)`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
As suggested by @herbelin.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
Also includes a minor fix of the Extraction doc (a Require was missing).
|
|
Minor clean up, no sense in having these as they do nothing.
|
|
|
|
|
|
|
|
|
|
|
|
We document the most useful timing targets and variables, how to invoke
them, and what the output looks like.
|
|
|
|
|
|
|
