Commit ceb6ca55 authored by Ralf Jung's avatar Ralf Jung

update warning settings, and fix warnings

parent e75c1713
Pipeline #33424 passed with stage
in 34 minutes and 2 seconds
-Q theories lrust
# We sometimes want to locally override notation, and there is no good way to do that with scopes.
-arg -w -arg -notation-overridden
# non-canonical projections (https://github.com/coq/coq/pull/10076) do not exist yet in 8.9.
# Cannot use non-canonical projections as it causes massive unification failures
# (https://github.com/coq/coq/issues/6294).
-arg -w -arg -redundant-canonical-projection
# change_no_check does not exist yet in 8.9.
-arg -w -arg -convert_concl_no_check
# "Declare Scope" does not exist yet in 8.9.
-arg -w -arg -undeclared-scope
theories/lifetime/model/definitions.v
theories/lifetime/model/faking.v
......
......@@ -9,6 +9,7 @@ Open Scope Z_scope.
Definition block : Set := positive.
Definition loc : Set := block * Z.
Declare Scope loc_scope.
Bind Scope loc_scope with loc.
Delimit Scope loc_scope with L.
Open Scope loc_scope.
......
......@@ -94,6 +94,6 @@ Notation "'letcall:' x := f args 'in' e" :=
we would even want them to print in general.
TODO: Introduce a Definition. *)
Notation "e1 '<-{Σ' i } '()'" := (e1 <- #i)%E
(only parsing, at level 80, format "e1 <-{Σ i } ()" ) : expr_scope.
(only parsing, at level 80) : expr_scope.
Notation "e1 '<-{Σ' i } e2" := (e1 <-{Σ i} () ;; e1+#1 <- e2)%E
(at level 80, format "e1 <-{Σ i } e2") : expr_scope.
......@@ -8,6 +8,7 @@ Set Default Proof Using "Type".
Definition elctx_elt : Type := lft * lft.
Notation elctx := (list elctx_elt).
Declare Scope lrust_elctx_scope.
Delimit Scope lrust_elctx_scope with EL.
(* We need to define [elctx] and [llctx] as notations to make eauto
work. But then, Coq is not able to bind them to their
......
......@@ -144,6 +144,7 @@ Qed.
Coercion ty_of_st : simple_type >-> type.
Declare Scope lrust_type_scope.
Delimit Scope lrust_type_scope with T.
Bind Scope lrust_type_scope with type.
......
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