diff options
| author | herbelin | 2008-10-26 13:43:06 +0000 |
|---|---|---|
| committer | herbelin | 2008-10-26 13:43:06 +0000 |
| commit | 20ba5a3934067925fb08d6d464ebe5102d358d41 (patch) | |
| tree | dd9982015c6e06746cebae65e0dce85a4e00e278 | |
| parent | 61035d6001dd784f1f1acf06aba84b3a06972301 (diff) | |
- MAJ svn:ignore pour bin/coq-parser (anciennement bin/parser)
- Correction test des scopes pour les notations récursives (suite commit 11489)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11506 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | toplevel/metasyntax.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/metasyntax.ml b/toplevel/metasyntax.ml index 920f6f4c54..4b4abe63ad 100644 --- a/toplevel/metasyntax.ml +++ b/toplevel/metasyntax.ml @@ -352,9 +352,9 @@ let analyse_notation_tokens l = let remove_extravars extrarecvars (vars,recvars) = let vars = List.fold_right (fun (x,y) l -> - if List.mem_assoc x l <> List.mem_assoc y recvars then + if List.assoc x l <> List.assoc y recvars then error - "Two end variables of a recursive notation are not in the same scope" + "Two end variables of a recursive notation are not in the same scope." else List.remove_assoc x l) extrarecvars (List.remove_assoc ldots_var vars) in |