diff options
| author | Son Ho | 2023-07-05 14:52:23 +0200 |
|---|---|---|
| committer | Son Ho | 2023-07-05 14:52:23 +0200 |
| commit | 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 (patch) | |
| tree | 43fb9284e8c02ec5ed8b8a5d59f6569d66b900ff /tests/coq | |
| parent | 442caaf62e4a217b9a10116c4e529c49f83c4efd (diff) | |
Start using namespaces in the Lean backend
Diffstat (limited to 'tests/coq')
| -rw-r--r-- | tests/coq/betree/BetreeMain_Opaque.v | 2 | ||||
| -rw-r--r-- | tests/coq/hashmap_on_disk/HashmapMain_Opaque.v | 2 | ||||
| -rw-r--r-- | tests/coq/misc/External_Opaque.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_Opaque.v index 08ab530a..51321f56 100644 --- a/tests/coq/betree/BetreeMain_Opaque.v +++ b/tests/coq/betree/BetreeMain_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: opaque function definitions *) +(** [betree_main]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. diff --git a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v index 6152b94b..e1e7fe2b 100644 --- a/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v +++ b/tests/coq/hashmap_on_disk/HashmapMain_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [hashmap_main]: opaque function definitions *) +(** [hashmap_main]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v index d60251e0..5ee65277 100644 --- a/tests/coq/misc/External_Opaque.v +++ b/tests/coq/misc/External_Opaque.v @@ -1,5 +1,5 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [external]: opaque function definitions *) +(** [external]: external function declarations *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. |