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

update Iris

parent af8b10ef
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
opam.pins
+ 1
− 1
View file @ 46efc427
coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 398bae9d092b6568cf8d504ca98d8810979eea33 coq-iris https://gitlab.mpi-sws.org/FP/iris-coq 2e2c5c25aea886acc7d0925d435fe856ffa6ac14
theories/typing/type.v
+ 1
− 1
View file @ 46efc427
...@@ -376,7 +376,7 @@ End type_contractive. ...@@ -376,7 +376,7 @@ End type_contractive.
(* Tactic automation. *) (* Tactic automation. *)
Ltac f_type_equiv := Ltac f_type_equiv :=
first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) | first [ ((eapply ty_size_type_dist || eapply ty_shr_type_dist || eapply ty_own_type_dist); try reflexivity) |
match goal with | |- @dist_later ?A ?n ?x ?y => match goal with | |- @dist_later ?A _ ?n ?x ?y =>
destruct n as [|n]; [exact I|change (@dist A _ n x y)] destruct n as [|n]; [exact I|change (@dist A _ n x y)]
end ]. end ].
Ltac solve_type_proper := Ltac solve_type_proper :=
......
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