From e7bef8ffabe48952aea91b49ccaa95e6e9f44d19 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 19 Sep 2003 00:00:23 +0000
Subject: parsing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4416 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/symbols.ml  | 2 +-
 interp/symbols.mli | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'interp')

diff --git a/interp/symbols.ml b/interp/symbols.ml
index 9d3766855b..07f45a7b64 100644
--- a/interp/symbols.ml
+++ b/interp/symbols.ml
@@ -40,7 +40,7 @@ open Ppextend
 (* Scope of symbols *)
 
 type scopes = scope_name list
-type level = precedence * precedence list
+type level = precedence * tolerability list
 type delimiters = string
 
 type scope = {
diff --git a/interp/symbols.mli b/interp/symbols.mli
index 3a3e3bc1ea..0f13c0d57e 100644
--- a/interp/symbols.mli
+++ b/interp/symbols.mli
@@ -27,7 +27,7 @@ open Ppextend
 (*s A scope is a set of interpreters for symbols + optional
    interpreter and printers for integers + optional delimiters *)
 
-type level = precedence * precedence list
+type level = precedence * tolerability list
 type delimiters = string
 type scope
 type scopes = scope_name list
-- 
cgit v1.2.3