Skip to content

Instantly share code, notes, and snippets.

@wires

wires/context.v

Created November 9, 2011 08:16
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/1350816 to your computer and use it in GitHub Desktop.
Save wires/1350816 to your computer and use it in GitHub Desktop.
Download ZIP
Coq strangeness when importing canonical_names
Raw
context.v
Section s1.
Context `{Ring R}. (* Error: Unbound and ungeneralizable variable Ring *)
(* That's a clear error message *)
End s1.
Require Import canonical_names.
Section s2.
Context `{Ring R}. (* Error: Cannot infer the type of R. *)
(* it haz confusing, why happens? *)
End s2.
@wires
Copy link
Author

wires commented Nov 10, 2011

This is caused by "Global Generalizable All Variables." (thanks robbertkrebbers)

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