From 6ad7e42acb577b06509499d73274556d700ebfe5 Mon Sep 17 00:00:00 2001 From: letouzey Date: Tue, 23 Apr 2013 18:16:04 +0000 Subject: Egramcoq: clean an ugly code snippet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16446 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/egramcoq.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/parsing/egramcoq.ml b/parsing/egramcoq.ml index 85e80dcb6..1b1c7dafd 100644 --- a/parsing/egramcoq.ml +++ b/parsing/egramcoq.ml @@ -292,12 +292,14 @@ let extend_grammar gram = let recover_notation_grammar ntn prec = let filter = function - | _, Notation (prec', vars, ng) when Notation.level_eq prec prec' && String.equal ntn ng.notgram_notation -> - Some (vars, ng) - | _ -> None in - let l = List.map_filter filter !grammar_state in - let () = match l with [_] -> () | _ -> assert false in - List.hd l + | _, Notation (prec', vars, ng) when + Notation.level_eq prec prec' && + String.equal ntn ng.notgram_notation -> Some (vars, ng) + | _ -> None + in + match List.map_filter filter !grammar_state with + | [x] -> x + | _ -> assert false (* Summary functions: the state of the lexer is included in that of the parser. Because the grammar affects the set of keywords when adding or removing -- cgit v1.2.3