Commit ac3cee05 authored by Ralf Jung's avatar Ralf Jung

silence fewer warnings, add comment about overwriting notation

parent 48758ab8
-Q theories stdpp
-arg -w -arg -notation-overridden,-redundant-canonical-projection,-several-object-files
-arg -w -arg -notation-overridden
theories/base.v
theories/tactics.v
theories/option.v
......
......@@ -380,6 +380,8 @@ Notation "1" := (Q2Qc 1) : Qc_scope.
Notation "2" := (1+1) : Qc_scope.
Notation "- 1" := (Qcopp 1) : Qc_scope.
Notation "- 2" := (Qcopp 2) : Qc_scope.
(* The following two already exist in Coq's stdlib, but we overwrite them with a
different definition. *)
Notation "x - y" := (x + -y) : Qc_scope.
Notation "x / y" := (x * /y) : Qc_scope.
Infix "≤" := Qcle : Qc_scope.
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment