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/extend.ml | |
| 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/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 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 = { |