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

fix deprecation warnings

parent acb6e71c
No related branches found
No related tags found
1 merge request!66bump to Coq 8.19
Pipeline #108188 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
theories/logrel/persistent_pred.v
+ 2
− 2
View file @ bd1a091f
...@@ -10,7 +10,7 @@ Section persistent_pred. ...@@ -10,7 +10,7 @@ Section persistent_pred.
pers_pred_car :> A → PROP; pers_pred_car :> A → PROP;
pers_pred_persistent x : Persistent (pers_pred_car x) pers_pred_persistent x : Persistent (pers_pred_car x)
}. }.
Local Arguments PersPred _%I {_}. Local Arguments PersPred _%_I {_}.
Global Existing Instances pers_pred_persistent. Global Existing Instances pers_pred_persistent.
Local Instance persistent_pred_equiv : Equiv persistent_pred := Local Instance persistent_pred_equiv : Equiv persistent_pred :=
...@@ -46,6 +46,6 @@ Section persistent_pred. ...@@ -46,6 +46,6 @@ Section persistent_pred.
End persistent_pred. End persistent_pred.
Global Arguments PersPred {_ _} _%I {_}. Global Arguments PersPred {_ _} _%_I {_}.
Global Arguments pers_pred_car {_ _} !_ _. Global Arguments pers_pred_car {_ _} !_ _.
Global Instance: Params (@pers_pred_car) 2 := {}. Global Instance: Params (@pers_pred_car) 2 := {}.
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment