From 0a0445c72e005c328b4764f5fb0f8f38e7a55d60 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Wed, 5 Jul 2023 14:52:23 +0200
Subject: Start using namespaces in the Lean backend

---
 tests/coq/misc/External_Opaque.v | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tests/coq/misc/External_Opaque.v')

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.
-- 
cgit v1.2.3


From 7c95800cefc87fad894f8bf855cfc047e713b3a7 Mon Sep 17 00:00:00 2001
From: Son Ho
Date: Thu, 6 Jul 2023 12:20:28 +0200
Subject: Improve the generated comments

---
 tests/coq/misc/External_Opaque.v | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'tests/coq/misc/External_Opaque.v')

diff --git a/tests/coq/misc/External_Opaque.v b/tests/coq/misc/External_Opaque.v
index 5ee65277..1224f426 100644
--- a/tests/coq/misc/External_Opaque.v
+++ b/tests/coq/misc/External_Opaque.v
@@ -8,27 +8,27 @@ Require Export External_Types.
 Import External_Types.
 Module External_Opaque.
 
-(** [core::mem::swap] *)
+(** [core::mem::swap]: forward function *)
 Axiom core_mem_swap_fwd :
   forall(T : Type), T -> T -> state -> result (state * unit)
 .
 
-(** [core::mem::swap] *)
+(** [core::mem::swap]: backward function 0 *)
 Axiom core_mem_swap_back0 :
   forall(T : Type), T -> T -> state -> state -> result (state * T)
 .
 
-(** [core::mem::swap] *)
+(** [core::mem::swap]: backward function 1 *)
 Axiom core_mem_swap_back1 :
   forall(T : Type), T -> T -> state -> state -> result (state * T)
 .
 
-(** [core::num::nonzero::NonZeroU32::{14}::new] *)
+(** [core::num::nonzero::NonZeroU32::{14}::new]: forward function *)
 Axiom core_num_nonzero_non_zero_u32_new_fwd
   : u32 -> state -> result (state * (option Core_num_nonzero_non_zero_u32_t))
 .
 
-(** [core::option::Option::{0}::unwrap] *)
+(** [core::option::Option::{0}::unwrap]: forward function *)
 Axiom core_option_option_unwrap_fwd :
   forall(T : Type), option T -> state -> result (state * T)
 .
-- 
cgit v1.2.3