Skip to content
Snippets Groups Projects
Commit a2d662ae authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan
Browse files

Revert "Make more uniform Arguments for type fields." 

This reverts commit a9f50489.
parent 850a722b
Branches
No related tags found
No related merge requests found
Pipeline #46517 passed
Stage: build
Hide whitespace changes
Inline Side-by-side
Showing
with 1 addition and 3 deletions
theories/typing/type.v
+ 1
− 3
View file @ a2d662ae
......@@ -50,9 +50,7 @@ Instance: Params (@ty_size) 2 := {}.
Instance: Params (@ty_own) 2 := {}.
Instance: Params (@ty_shr) 2 := {}.
Arguments ty_size {_ _} _ / : simpl nomatch.
Arguments ty_own {_ _} _ _ _ / : simpl nomatch.
Arguments ty_shr {_ _} _ _ _ _ / : simpl nomatch.
Arguments ty_own {_ _} !_ _ _ / : simpl nomatch.
Class TyWf `{!typeG Σ} (ty : type) := { ty_lfts : list lft; ty_wf_E : elctx }.
Arguments ty_lfts {_ _} _ {_}.
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment