coq export: add mappings of erasing.lp in rmap if possible (#1040)

Deducteam · Feb 1, 2024 · a140014 · a140014
1 parent bc447c9
commit a140014
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)