coq export: treat P_NLit as P_Iden (#1015)

Deducteam · Oct 25, 2023 · 8dc823f · 8dc823f
1 parent 8481cd5
commit 8dc823f
Show file tree

Hide file tree

Showing 2 changed files with 10 additions and 4 deletions.
diff --git a/doc/options.rst b/doc/options.rst
@@ -129,7 +129,7 @@ It instructs Lambdapi to replace any occurrence of the unqualified identifier ``
 
 if the symbols corresponding to the builtins ``"arr"``, ``"imp"`` and ``"all"`` occurs partially applied in the input file. Example: `coq.v <https://github.com/Deducteam/lambdapi/blob/master/libraries/coq.v>`__.
 
-* ``--erasing <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations like for the option ``--renaming`` except that, this time, ``lp_id`` can be a qualified identifier. It has the same effect as the option ``--renaming`` plus it removes any declaration of the renamed symbols. ``coq_expr`` therefore needs to be defined in Coq standard library or in the Coq file specified with the option ``-requiring``. It is not necessary to have entries for the symbols corresponding to the builtins ``"El"`` and ``"Prf"`` declared with the option ``--encoding`` since they are erased automatically. Example: `erasing.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/erasing.lp>`__.
+* ``--erasing <LP_FILE>`` where ``<LP_FILE>`` contains a sequence of builtin declarations like for the option ``--renaming`` except that, this time, ``lp_id`` can be a qualified identifier. It has the same effect as the option ``--renaming`` plus it removes any declaration of the renamed symbols. ``coq_expr`` therefore needs to be defined in Coq standard library or in the Coq file specified with the option ``--requiring``. It is not necessary to have entries for the symbols corresponding to the builtins ``"El"`` and ``"Prf"`` declared with the option ``--encoding`` since they are erased automatically. Example: `erasing.lp <https://github.com/Deducteam/lambdapi/blob/master/libraries/erasing.lp>`__.
 
 * ``--use-notations`` instructs Lambdapi to use the usual Coq notations for the symbols corresponding to the builtins ``"eq"``, ``"not"``, ``"and"`` and ``"or"``.
 

diff --git a/src/export/coq.ml b/src/export/coq.ml
@@ -94,8 +94,9 @@ let set_erasing : string -> unit = fun f ->
     | {elt=P_builtin(coq_id,lp_qid);_} ->
         if Logger.log_enabled() then
           log "rename %a into %s" Pretty.qident lp_qid coq_id;
-        if Logger.log_enabled() then log "erase %s" (snd lp_qid.elt);
-        erase := StrSet.add (snd lp_qid.elt) !erase;
+        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
     | {pos;_} -> fatal pos "Invalid command."
   in
@@ -194,7 +195,12 @@ let rec term : p_term pp = fun ppf t ->
   | P_Expl _ -> wrn t.pos "TODO"; assert false
   | P_Type -> out ppf "Type"
   | P_Wild -> out ppf "_"
-  | P_NLit i -> raw_ident ppf i
+  | P_NLit i ->
+      if !stt then
+        match QidMap.find_opt ([],i) !map_erased_qid_coq with
+        | Some s -> string ppf s
+        | None -> raw_ident ppf i
+      else raw_ident ppf i
   | P_Iden(qid,b) ->
       if b then out ppf "@@";
       if !stt then