Skip to content

Instantly share code, notes, and snippets.

@wires

wires/*scratch*

Created November 10, 2011 16:32
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save wires/1355310 to your computer and use it in GitHub Desktop.
Save wires/1355310 to your computer and use it in GitHub Desktop.
Download ZIP
strange behaviour for coq library Bvector
Raw
*scratch*
(* http://coq.inria.fr/stdlib/Coq.Bool.Bvector.html
Section VECTORS --> Vcons, Vextend -- this I cannot use?
Section BOOLEAN_VECTORS --> Bcons -- this I can use
*)
Require Import Bvector.
Check (Bcons).
Check (Vcons). (* Error: The reference Vcons was not found
in the current environment. *)
Check (Vextend). (* same error*)
@wires
Copy link
Author

wires commented Nov 10, 2011

Caused by coq/coq@05085e8
Thanks tomprince

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment