fix (non) export of integer literals to coq and dk

src/export/coq.ml

@@ -211,14 +211,9 @@ let rec term oc t =
   | P_Patt _ -> wrn t.pos "TODO"; assert false
   | P_Expl _ -> wrn t.pos "TODO"; assert false
   | P_SLit _ -> wrn t.pos "TODO"; assert false
+  | P_NLit _ -> wrn t.pos "TODO"; assert false
   | P_Type -> string oc "Type"
   | P_Wild -> char oc '_'
-  | P_NLit i ->
-      if !stt then
-        match QidMap.find_opt ([],i) !map_erased_qid_coq with
-        | Some s -> string oc s
-        | None -> raw_ident oc i
-      else raw_ident oc i
   | P_Iden(qid,b) ->
       if b then char oc '@';
       if !stt then

src/export/rawdk.ml

@@ -25,7 +25,7 @@ let rec term : p_term pp = fun ppf t ->
   | P_Expl u -> out ppf "(%a)" term u
   | P_Type -> out ppf "Type"
   | P_Wild -> out ppf "_"
-  | P_NLit i -> string ppf i
+  | P_NLit _ -> fatal t.pos "Cannot translate integer literals."
   | P_SLit _ -> fatal t.pos "Cannot translate string literals."
   | P_Iden(qid,_) -> qident ppf qid
   | P_Arro(u,v) -> out ppf "%a -> %a" pterm u term v

src/handle/command.ml

@@ -124,10 +124,11 @@ let handle_require_as :
       {ss with alias_path; path_alias}
     end
 
-(** [handle_require compile bo ss p] handles the command [require p as id]
-    with [ss] as signature state and [compile] as compilation function (passed
-    as argument to avoid cyclic dependencies). On success, an updated
-    signature state is returned. *)
+(** [handle_require compile bo ss p] handles the command [require p] with
+    [compile] as compilation function (passed as argument to avoid cyclic
+    dependencies), [bo=Some(true)] if the command is [require private open p],
+    [bo=Some(false)] if the command is [require open p], and [ss] as signature
+    state. On success, an updated signature state is returned. *)
 let handle_require compile bo ss {elt=p;_} =
   let ss = rec_require compile ss p in
   match bo with