Extraction: minor tweaks to ease ongoing experiments about Lambda

 - Common.get_native_char instead of just a pp function of this char

 - Enrich the record projection table

1 files changed, 4 insertions, 2 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index 135d3fc7cd..4f78ffe978 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -642,11 +642,13 @@ let is_native_char = function
     MutInd.equal kn ind_ascii && check_extract_ascii () && is_list_cons l
   | _ -> false
 
-let pp_native_char c =
+let get_native_char c =
   let rec cumul = function
     | [] -> 0
     | MLcons(_,ConstructRef(_,j),[])::l -> (2-j) + 2 * (cumul l)
     | _ -> assert false
   in
   let l = match c with MLcons(_,_,l) -> l | _ -> assert false in
-  str ("'"^Char.escaped (Char.chr (cumul l))^"'")
+  Char.chr (cumul l)
+
+let pp_native_char c = str ("'"^Char.escaped (get_native_char c)^"'")