diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-24 23:50:27 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-24 23:50:27 +0000 |
| commit | 55a483ea0694eab627e9386f69f3c05693e37fa1 (patch) | |
| tree | 462f8dc9b8a8f02a76ef38c41ab9cc896dab2960 /parsing | |
| parent | 475e5a78b5b410cfa437bb89b1aebf36e01d5950 (diff) | |
Rétablissement printer via ast
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3272 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -rw-r--r-- | parsing/g_natsyntax.ml | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index cc68038e7..395f1c0c5 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" |