From eeef625099957a003f4926a8d382c2fd538ce439 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Sat, 4 Apr 2020 00:31:30 +0200
Subject: [PATCH] Remove obsolete comment and arguments command.

---
 theories/vector.v | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/theories/vector.v b/theories/vector.v
index 17f1b8f1..db1f678e 100644
--- a/theories/vector.v
+++ b/theories/vector.v
@@ -41,9 +41,6 @@ Proof.
   refine match v with [#] => tt | x ::: v => λ P Hcons, Hcons x v end.
 Defined.
 
-(** Notice that we cannot define [Vector.nth] as an instance of our [Lookup]
-type class, as it has a dependent type. *)
-Arguments Vector.nth {_ _} !_ !_%fin /.
 Instance vector_lookup_total A : ∀ m, LookupTotal (fin m) A (vec A m) :=
   fix go m i {struct i} := let _ : ∀ m, LookupTotal _ _ _ := @go in
   match i in fin m return vec A m → A with
-- 
GitLab