Skip to content
Snippets Groups Projects

Explicitly Require Coq Vector in vector.v (for coq/coq#18936)

Merged Andres Erbsen requested to merge andres-erbsen/stdpp:require-vector into master
1 unresolved thread
1 file
+ 3
0
Compare changes
  • Side-by-side
  • Inline
+ 3
0
@@ -2,6 +2,9 @@
@@ -2,6 +2,9 @@
(lists of fixed length). It uses the definitions from the standard library, but
(lists of fixed length). It uses the definitions from the standard library, but
renames or changes their notations, so that it becomes more consistent with the
renames or changes their notations, so that it becomes more consistent with the
naming conventions in this development. *)
naming conventions in this development. *)
 
(* Coq warns about using vector, but it is not deprecated. Instead somehow they seem concerned
 
about people having too much fun with type indices. See
 
<https://github.com/coq/coq/pull/18032> for discussion. Let's just silence that. *)
Local Set Warnings "-stdlib-vector".
Local Set Warnings "-stdlib-vector".
From Coq Require Vector.
From Coq Require Vector.
From stdpp Require Import countable.
From stdpp Require Import countable.
Loading