diff options
Diffstat (limited to 'tests/coq/misc/External_Funs.v')
| -rw-r--r-- | tests/coq/misc/External_Funs.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/tests/coq/misc/External_Funs.v b/tests/coq/misc/External_Funs.v index 0a14c7d1..8a3360bb 100644 --- a/tests/coq/misc/External_Funs.v +++ b/tests/coq/misc/External_Funs.v @@ -8,8 +8,8 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export External_Types. Import External_Types. -Require Export External_Opaque. -Import External_Opaque. +Require Export External_FunsExternal. +Import External_FunsExternal. Module External_Funs. (** [external::swap]: forward function |