From f929791a2ce1c74ac28a832bfe48ff07821f096f Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 15 Oct 2012 17:10:00 +0000
Subject: 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
---
 grammar/tacextend.ml4 | 10 +++++-----
 1 file 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:
-- 
cgit v1.2.3