From 55a483ea0694eab627e9386f69f3c05693e37fa1 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 24 Nov 2002 23:50:27 +0000
Subject: Rétablissement printer via ast

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3272 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_natsyntax.ml | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml
index cc68038e78..395f1c0c51 100644
--- a/parsing/g_natsyntax.ml
+++ b/parsing/g_natsyntax.ml
@@ -10,7 +10,7 @@
 
 (* This file to allow writing (3) for (S (S (S O))) 
    and still write (S y) for (S y) *)
-(*
+
 open Pcoq
 open Pp
 open Util
@@ -21,6 +21,9 @@ open Coqlib
 open Termast
 open Extend
 
+let ast_O = ast_of_ref glob_O
+let ast_S = ast_of_ref glob_S
+
 (* For example, (nat_of_string "3") is <<(S (S (S O)))>> *)
 let nat_of_int n dloc =
   let ast_O = set_loc dloc ast_O in
@@ -82,7 +85,7 @@ let nat_printer std_pr p =
     | None -> pr_S (pr_external_S std_pr p)
 
 let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer)
-
+(*
 (* Declare the primitive parser *)
 
 let unat = create_univ_if_new "nat"
-- 
cgit v1.2.3