diff options
| -rw-r--r-- | parsing/extend.ml | 7 | ||||
| -rw-r--r-- | parsing/g_natsyntax.ml | 4 |
2 files changed, 5 insertions, 6 deletions
diff --git a/parsing/extend.ml b/parsing/extend.ml index 2cde3e24e9..a689a59338 100644 --- a/parsing/extend.ml +++ b/parsing/extend.ml @@ -262,12 +262,11 @@ let rec subst_hunk subst_pat subst hunk = match hunk with highest precedence), and the child's one, follow the given relation. *) -let compare_prec a1 a2 = a1-a2 - let tolerable_prec oparent_prec_reln child_prec = match oparent_prec_reln with - | Some (pprec, L) -> (compare_prec child_prec pprec) < 0 - | Some (pprec, E) -> (compare_prec child_prec pprec) <= 0 + | Some (pprec, L) -> child_prec < pprec + | Some (pprec, E) -> child_prec <= pprec + | Some (_, Prec level) -> child_prec <= level | _ -> true type 'pat syntax_entry = { diff --git a/parsing/g_natsyntax.ml b/parsing/g_natsyntax.ml index 395f1c0c51..1d91a949f9 100644 --- a/parsing/g_natsyntax.ml +++ b/parsing/g_natsyntax.ml @@ -72,7 +72,7 @@ let int_of_nat p = let pr_S a = hov 0 (str "S" ++ brk (1,1) ++ a) let rec pr_external_S std_pr = function - | Node (l,"APPLIST", [b; a]) when b = ast_S -> + | Node (l,"APPLIST", [b; a]) when alpha_eq (b,ast_S) -> str"(" ++ pr_S (pr_external_S std_pr a) ++ str")" | p -> std_pr p @@ -82,7 +82,7 @@ let rec pr_external_S std_pr = function let nat_printer std_pr p = match (int_of_nat p) with | Some i -> str "(" ++ str (string_of_int i) ++ str ")" - | None -> pr_S (pr_external_S std_pr p) + | None -> str "(" ++ pr_S (pr_external_S std_pr p) ++ str ")" let _ = Esyntax.Ppprim.add ("nat_printer", nat_printer) (* |