diff options
| author | herbelin | 2005-12-22 18:45:54 +0000 |
|---|---|---|
| committer | herbelin | 2005-12-22 18:45:54 +0000 |
| commit | 749fc73f1fcc1690532e8a38af0a635341a6e791 (patch) | |
| tree | a7db571c970c1fe14c83ba14a1dcdcbf0b1af354 | |
| parent | 21aca613bc898b501b132e4f455e8aa6c89729ef (diff) | |
Double bug de interp_modifiers anciennement caché par un troisième que les nouveaux warnings de ocaml 3.09 avaient révélé
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7696 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index b5fd0d5708..ad5ae7c605 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -681,7 +681,7 @@ let (inSyntaxExtension, outSyntaxExtension) = (**************************************************************************) (* Precedences *) -let interp_modifiers = +let interp_modifiers modl = let onlyparsing = ref false in let rec interp assoc level etyps format = function | [] -> @@ -710,9 +710,8 @@ let interp_modifiers = interp assoc level etyps format l | SetFormat s :: l -> if format <> None then error "A format is given more than once"; - onlyparsing := true; interp assoc level etyps (Some s) l - in interp None None [] None + in interp None None [] None modl let merge_modifiers a n l = (match a with None -> [] | Some a -> [SetAssoc a]) @ |