| Age | Commit message (Collapse) | Author |
|---|
|
to escape non-UTF-8 file names)
|
|
|
|
We don't gain anything from the kernel yet as transparent constants
_do_ require the `side_eff` exporting machinery.
Next step, understand why.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
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)`.
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
