diff options
Diffstat (limited to 'parsing/g_natsyntax.ml')
| -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" |