From f3c60be7e370b20cccbb006d3cba907e15659656 Mon Sep 17 00:00:00 2001
From: Xavier Leroy <xavier.leroy@inria.fr>
Date: Mon, 28 Aug 2017 15:05:27 +0200
Subject: Issue #199: improve namespace management for clightgen-produced files

Qualify imports in clightgen-produced files and in Clightdefs so that they can be used with coq -Q /path/to/compcert compcert.
Remove 'Require Export' from Clightdefs as suggested in issue #199.
---
 exportclight/Clightdefs.v    | 13 ++-----------
 exportclight/ExportClight.ml |  9 ++++-----
 2 files changed, 6 insertions(+), 16 deletions(-)

(limited to 'exportclight')

diff --git a/exportclight/Clightdefs.v b/exportclight/Clightdefs.v
index 1124fae8..83d82d88 100644
--- a/exportclight/Clightdefs.v
+++ b/exportclight/Clightdefs.v
@@ -15,17 +15,8 @@
 
 (** All imports and definitions used by .v Clight files generated by clightgen *)
 
-Require Export String.
-Require Export List.
-Require Export ZArith.
-Require Export Integers.
-Require Export Floats.
-Require Export AST.
-Require Export Ctypes.
-Require Export Cop.
-Require Export Clight.
-Require Import Maps.
-Require Import Errors.
+From Coq Require Import String List ZArith.
+From compcert Require Import Integers Floats Maps Errors AST Ctypes Cop Clight.
 
 Definition tvoid := Tvoid.
 Definition tschar := Tint I8 Signed noattr.
diff --git a/exportclight/ExportClight.ml b/exportclight/ExportClight.ml
index 3136ed54..16aac9ab 100644
--- a/exportclight/ExportClight.ml
+++ b/exportclight/ExportClight.ml
@@ -478,12 +478,11 @@ let print_assertions p =
 
 (* The prologue *)
 
-let prologue = "\n\
-Require Import Clightdefs.\n\
-\
+let prologue = "\
+From Coq Require Import String List ZArith.\n\
+From compcert Require Import Coqlib Integers Floats AST Ctypes Cop Clight Clightdefs.\n\
 Local Open Scope Z_scope.\n\
-\
-"
+\n"
 
 (* Naming the compiler-generated temporaries occurring in the program *)
 
-- 
cgit