From f6f537dd60336b599c9541b0dca56255bdf2ba5e Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Mon, 27 Aug 2018 11:13:47 -0400 Subject: Import prim token notations before using them This is required for compatibility with https://github.com/coq/coq/pull/8064, where prim token notations no longer follow `Require`, but instead follow `Import`. Closes #246 Closes #250 --- cfrontend/SimplLocals.v | 1 + 1 file changed, 1 insertion(+) (limited to 'cfrontend/SimplLocals.v') diff --git a/cfrontend/SimplLocals.v b/cfrontend/SimplLocals.v index b142d3cc..f54aa60d 100644 --- a/cfrontend/SimplLocals.v +++ b/cfrontend/SimplLocals.v @@ -22,6 +22,7 @@ Require Compopts. Open Scope error_monad_scope. Open Scope string_scope. +Open Scope list_scope. Module VSet := FSetAVL.Make(OrderedPositive). -- cgit