Commit 934da1dd authored by Pierre Letouzey's avatar Pierre Letouzey
Browse files

An extra Open Scope for fixing the compilation with Coq 8.11

parent 82720a0e
......@@ -26,6 +26,7 @@ Qed.
Import Names.
Import Logic. (* for [eq] *)
Local Open Scope nat. (* needed for Coq 8.11 *)
Lemma mem_false x vs :
~In x vs -> mem x vs = false.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment