diff options
Diffstat (limited to 'parsing/extend.ml')
| -rw-r--r-- | parsing/extend.ml | 7 |
1 files changed, 3 insertions, 4 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 = { |