| Commit message (Collapse) | Author | Age |
|---|
| |\
| |
| |
| | |
(clause "where" with implicit arguments)
|
| | |
| |
| |
| |
| |
| |
| |
| |
| |
| | |
The file links.v is using utf-8 characters so this is needed at least
to test this file. For the other files, it is not completely without
effect since it makes that symbols like => and forall are respectively
displayed ⇒ and ∀.
Maybe tests with iso-8859-1 or test without a charset option should be
kept.
|
| |/
|
|
|
|
|
|
| |
PR #1120 was still buggy for the following reasons: variables in the
lhs of the notation were linked in the glob file while they have
nowhere to link to (the binder is the notation string) [I thought the
change I commited in links.html.out was actually improving but it was
an overlook, sorry.]
|
| |
|
|
|
|
|
|
|
|
|
|
|
| |
This allows e.g. the following to work:
Reserved Notation "* a" (at level 70).
Inductive P {n : nat} : nat -> Prop := c m : *m where "* m" := (P m).
We seize this opportunity to make main calls to Metasyntax to depend
on an arbitrary env rather than on Global.env.
Incidentally, this fixes a little coqdoc bug in classifying the
inductive type referred to in the "where" clause.
|
|
|
One file was already ready for testing. We add another one.
Note that we have to remove the machine-dependent lines in the output
tex files.
|
Maxime Dénès
Hugo Herbelin