diff options
| author | letouzey | 2012-10-15 17:10:00 +0000 |
|---|---|---|
| committer | letouzey | 2012-10-15 17:10:00 +0000 |
| commit | f929791a2ce1c74ac28a832bfe48ff07821f096f (patch) | |
| tree | 6b336db73b0d92f1d8206ce479f6be3ced6d22e5 | |
| parent | 5c621142ba5f48c168e69b5a1b871f3f55fec2b7 (diff) | |
Stylistic improvement: avoid a "if match List.hd"
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15889 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | grammar/tacextend.ml4 | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 5500a233a3..e50ea27e55 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -215,12 +215,12 @@ EXTEND declare_tactic loc s l ] ] ; tacrule: - [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" - -> - if match List.hd l with GramNonTerminal _ -> true | _ -> false then + [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" -> + (match l with + | GramNonTerminal _ :: _ -> (* En attendant la syntaxe de tacticielles *) - failwith "Tactic syntax must start with an identifier"; - (l,e) + failwith "Tactic syntax must start with an identifier" + | _ -> (l,e)) ] ] ; tacargs: |