diff options
Diffstat (limited to '')
| -rw-r--r-- | tests/coq/betree/BetreeMain_FunsExternal.v (renamed from tests/coq/betree/BetreeMain_Opaque.v) | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/tests/coq/betree/BetreeMain_Opaque.v b/tests/coq/betree/BetreeMain_FunsExternal.v index a065c8a3..07dba263 100644 --- a/tests/coq/betree/BetreeMain_Opaque.v +++ b/tests/coq/betree/BetreeMain_FunsExternal.v @@ -1,5 +1,6 @@ (** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *) -(** [betree_main]: external function declarations *) +(** [betree_main]: external functions. +-- This is a template file: rename it to "FunsExternal.lean" and fill the holes. *) Require Import Primitives. Import Primitives. Require Import Coq.ZArith.ZArith. @@ -8,7 +9,7 @@ Import ListNotations. Local Open Scope Primitives_scope. Require Export BetreeMain_Types. Import BetreeMain_Types. -Module BetreeMain_Opaque. +Module BetreeMain_FunsExternal. (** [betree_main::betree_utils::load_internal_node]: forward function Source: 'src/betree_utils.rs', lines 98:0-98:63 *) @@ -42,4 +43,4 @@ Axiom core_option_Option_unwrap : forall(T : Type), option T -> state -> result (state * T) . -End BetreeMain_Opaque . +End BetreeMain_FunsExternal. |