From 29b75ca42b7824f5feec24df5ecc7cd75cb78251 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 23 Dec 2005 10:43:37 +0000
Subject: Simplifification de vernac_expr li  l'abandon du traducteur

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7712 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/notation.mli | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

(limited to 'interp/notation.mli')

diff --git a/interp/notation.mli b/interp/notation.mli
index 0e401acd6e..896d427932 100644
--- a/interp/notation.mli
+++ b/interp/notation.mli
@@ -88,7 +88,7 @@ type interp_rule =
   | NotationRule of scope_name option * notation
   | SynDefRule of kernel_name
 val declare_notation_interpretation : notation -> scope_name option ->
-      interpretation -> dir_path * string -> bool -> unit
+      interpretation -> dir_path * string -> unit
 
 val declare_uninterpretation : interp_rule -> interpretation -> unit
 
@@ -111,15 +111,14 @@ val availability_of_notation : scope_name option * notation -> scopes ->
 
 (*s Declare and test the level of a (possibly uninterpreted) notation *)
 
-val declare_notation_level : notation -> level option * level -> unit
-val level_of_notation : notation -> level option * level 
-      (* raise [Not_found] if no level *)
+val declare_notation_level : notation -> level -> unit
+val level_of_notation : notation -> level (* raise [Not_found] if no level *)
 
 (*s** Miscellaneous *)
 
 (* Checks for already existing notations *)
 val exists_notation_in_scope : scope_name option -> notation ->
-      interpretation -> bool * bool
+      interpretation -> bool
 
 (* Declares and looks for scopes associated to arguments of a global ref *)
 val declare_arguments_scope: global_reference -> scope_name option list -> unit
-- 
cgit v1.2.3