diff options
| author | herbelin | 2005-12-23 10:43:37 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-23 10:43:37 +0000 |
| commit | 29b75ca42b7824f5feec24df5ecc7cd75cb78251 (patch) | |
| tree | 7b292623378acfb1c70cb692ba4a13290381eeef /interp/notation.mli | |
| parent | c506c385473224345526bfff4b71c56222ccbb11 (diff) | |
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
Diffstat (limited to 'interp/notation.mli')
| -rw-r--r-- | interp/notation.mli | 9 |
1 files changed, 4 insertions, 5 deletions
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 |