Skip to content
Snippets Groups Projects
Commit b86dfeb8 authored by Ralf Jung's avatar Ralf Jung
Browse files

update for warnings

parent 1c4c08c4
Branches
No related tags found
No related merge requests found
Pipeline #108240 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
_CoqProject
+ 2
− 2
View file @ b86dfeb8
-Q solutions solutions -Q solutions solutions
-Q exercises exercises -Q exercises exercises
-docroot tutorial-popl20 -docroot tutorial-popl20
# Fixing this one requires Coq 8.19 # Warning seems incorrect, see https://gitlab.mpi-sws.org/iris/stdpp/-/issues/216
-arg -w -arg -argument-scope-delimiter -arg -w -arg -notation-incompatible-prefix
solutions/language.v solutions/language.v
solutions/polymorphism.v solutions/polymorphism.v
......
exercises/sem_types.v
+ 1
− 1
View file @ b86dfeb8
...@@ -41,7 +41,7 @@ Record sem_ty Σ := SemTy { ...@@ -41,7 +41,7 @@ Record sem_ty Σ := SemTy {
sem_ty_car :> val → iProp Σ; sem_ty_car :> val → iProp Σ;
sem_ty_persistent v : Persistent (sem_ty_car v) sem_ty_persistent v : Persistent (sem_ty_car v)
}. }.
Arguments SemTy {_} _%I {_}. Arguments SemTy {_} _%_I {_}.
Arguments sem_ty_car {_} _ _ : simpl never. Arguments sem_ty_car {_} _ _ : simpl never.
(** Iris uses the type class [Persistent] to capture which propositions are (** Iris uses the type class [Persistent] to capture which propositions are
......
solutions/sem_types.v
+ 1
− 1
View file @ b86dfeb8
...@@ -41,7 +41,7 @@ Record sem_ty Σ := SemTy { ...@@ -41,7 +41,7 @@ Record sem_ty Σ := SemTy {
sem_ty_car :> val → iProp Σ; sem_ty_car :> val → iProp Σ;
sem_ty_persistent v : Persistent (sem_ty_car v) sem_ty_persistent v : Persistent (sem_ty_car v)
}. }.
Arguments SemTy {_} _%I {_}. Arguments SemTy {_} _%_I {_}.
Arguments sem_ty_car {_} _ _ : simpl never. Arguments sem_ty_car {_} _ _ : simpl never.
(** Iris uses the type class [Persistent] to capture which propositions are (** Iris uses the type class [Persistent] to capture which propositions are
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment