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

fix deprecation warning

parent 26aeece9
No related branches found
No related tags found
1 merge request!67bump to Coq 8.20
Pipeline #108212 passed
Hide whitespace changes
Inline Side-by-side
theories/logrel/F_mu_ref_conc/typing.v
+ 2
− 2
View file @ 9943d6b5
...@@ -147,7 +147,7 @@ Proof. ...@@ -147,7 +147,7 @@ Proof.
match goal with H : context[_ → _ ⊢ₜ _ : _] |- _ => rename H into IH end. match goal with H : context[_ → _ ⊢ₜ _ : _] |- _ => rename H into IH end.
specialize (IH specialize (IH
(subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)). (subst (ren (+1)) <$> Γ1) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
rewrite ?map_length in IH. rewrite ?length_map in IH.
repeat rewrite fmap_app. apply IH. repeat rewrite fmap_app. apply IH.
by repeat rewrite fmap_app. by repeat rewrite fmap_app.
- econstructor; eauto. - econstructor; eauto.
...@@ -155,7 +155,7 @@ Proof. ...@@ -155,7 +155,7 @@ Proof.
match goal with H : context[_ → _ ⊢ₜ _ : TExist ?t] |- _ => rename t into τ end. match goal with H : context[_ → _ ⊢ₜ _ : TExist ?t] |- _ => rename t into τ end.
specialize (IH specialize (IH
(τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)). (τ :: (subst (ren (+1)) <$> Γ1)) (subst (ren (+1)) <$> Γ2) (subst (ren (+1)) <$> ξ)).
asimpl in IH. rewrite ?map_length in IH. asimpl in IH. rewrite ?length_map in IH.
repeat rewrite fmap_app. apply IH. repeat rewrite fmap_app. apply IH.
by repeat rewrite fmap_app. by repeat rewrite fmap_app.
Qed. Qed.
......
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