coq export: add mappings of erasing.lp in rmap if possible

fblanqui · Feb 1, 2024 · 9c13c6e · 9c13c6e
1 parent bc447c9
commit 9c13c6e
Showing 1 changed file with 3 additions and 1 deletion.
diff --git 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)