From 9c13c6e1ca6d0e1dcef9e8bff19930cc837d508f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Fr=C3=A9d=C3=A9ric=20Blanqui?= <frederic.blanqui@inria.fr>
Date: Thu, 1 Feb 2024 12:07:17 +0100
Subject: [PATCH] coq export: add mappings of erasing.lp in rmap if possible

---
 src/export/coq.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/src/export/coq.ml b/src/export/coq.ml
index 1e6499f0a..9a6f51bd9 100644
--- a/src/export/coq.ml
+++ b/src/export/coq.ml
@@ -97,7 +97,9 @@ let set_erasing : string -> unit = fun f ->
         let id = snd lp_qid.elt in
         if Logger.log_enabled() then log "erase %s" id;
         erase := StrSet.add id !erase;
-        map_erased_qid_coq := QidMap.add lp_qid.elt coq_id !map_erased_qid_coq
+        map_erased_qid_coq := QidMap.add lp_qid.elt coq_id !map_erased_qid_coq;
+        if fst lp_qid.elt = [] && id <> coq_id then
+          rmap := StrMap.add id coq_id !rmap
     | {pos;_} -> fatal pos "Invalid command."
   in
   Stream.iter consume (Parser.parse_file f)