diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 18:48:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2002-11-26 18:48:47 +0000 |
| commit | c6b910e54986d2f5b2d6615c2a8a159b4c55731d (patch) | |
| tree | 10329bcfdd3a6381121ce59e1c289e950a678b11 /parsing | |
| parent | 6331212594ab882e83c9817e9b244d0e984feb2e (diff) | |
Oubli
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3300 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'parsing')
| -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 2cde3e24e..a689a5933 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 395f1c0c5..1d91a949f 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) (* |