diff options
| -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: |