xavierleroy / coq2html Goto Github PK

Dear Xavier,

@palmskog requested here: (coq/platform#17) to include your development into the Coq Platform, which is the standard user facing distribution of Coq.

Coq Platform has a "full" and "extended" level. Inclusion in the "full" level requires an explicit statement by the maintainers, that they agree to the charter of the Coq Platform and intend to publish compatible releases for each release of Coq in a reasonable time frame. For the "extended" level the rules are more relaxed. For developments in the "full" level, users should be able to rely on that the package is maintained, so that they can base their own development on it without a large risk that they have to factor it out again later cause of maintenance issues.

Can you please comment in the Coq Platform issue mentioned above if you do want your package included in the Coq Platform in agreement to the Coq Platform charter, and if so which level you would prefer?

Best regards,

Michael

coq2html gets confused when unicode characters are used in identifiers. Here is a small example

Inductive ωtruth :=
| ωtrue : ωtruth
| ωfalse : ωtruth
| otrue : ωtruth
| ofalse : ωtruth.
Definition otruth := ωtruth.

Reserved Notation  "'¬' t" (at level 50).
Definition ωneg (ω:ωtruth) : ωtruth :=
  match ω with
  | ωtrue => ωfalse
  | ωfalse => ωtrue
  | otrue => ofalse
  | ofalse => otrue
  end.
Notation  "'¬' x" := (ωneg x).
Definition oneg := ωneg.

Lemma ωdoubleneg :
  forall (ω:ωtruth), ¬(¬ω) = ω.
Proof.
  destruct ω; reflexivity.
Qed.

Lemma odoubleneg :
  forall (o:otruth), oneg (oneg o) = o.
Proof.
  destruct o; reflexivity.
Qed.

The o-prefixed identifiers are handled properly but not the ω-prefixed ones.

It would be nice to have the Variant keyword recognized, and highlighted as the Inductive keyword in the output html.
Currently, this doesn't seem to be the case. The fix may be as simple as adding it to the coq_keywords set.