From c6b910e54986d2f5b2d6615c2a8a159b4c55731d Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Tue, 26 Nov 2002 18:48:47 +0000
Subject: Oubli

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3300 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/extend.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

(limited to 'parsing/extend.ml')

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 = {
-- 
cgit v1.2.3