diff --git a/theories/algebra/lib/gmap_view.v b/theories/algebra/lib/gmap_view.v index a3a7b544f94f37f52963eb5476032bb839f23f95..55f3962a131c547886c7c4416ae2485f7cb5c7f7 100644 --- a/theories/algebra/lib/gmap_view.v +++ b/theories/algebra/lib/gmap_view.v @@ -205,7 +205,7 @@ Section lemmas. rewrite /gmap_view_auth /gmap_view_frag. rewrite view_both_valid. setoid_rewrite gmap_view_rel_lookup. split; intros Hm; split. - - apply (Hm 0). + - apply (Hm 0%nat). - apply equiv_dist=>n. apply Hm. - apply Hm. - revert n. apply equiv_dist. apply Hm.