diff options
| -rw-r--r-- | parsing/egrammar.ml | 8 | ||||
| -rw-r--r-- | parsing/g_basevernac.ml4 | 2 | ||||
| -rw-r--r-- | parsing/g_vernacnew.ml4 | 2 | ||||
| -rw-r--r-- | parsing/tacextend.ml4 | 8 |
4 files changed, 14 insertions, 6 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index aa2558ddab..1acf41ec6c 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -438,16 +438,20 @@ let get_tactic_entry n = open Tacexpr +let head_is_ident = function (_,VTerm _::_,_) -> true | _ -> false + let add_tactic_entries (lev,gl) = let univ = get_univ "tactic" in let entry, pos = get_tactic_entry lev in let rules = - if lev = 0 then + if lev = 0 then begin + if not (List.for_all head_is_ident gl) then + error "Notations for simple tactics must start with an identifier"; let make_act s tac loc l = (TacAlias(loc,s,l,tac):raw_atomic_tactic_expr) in let f (s,l,tac) = make_rule univ (make_act s tac) (make_vprod_item lev "tactic") l in - List.map f gl + List.map f gl end else let make_act s tac loc l = (TacAtom(loc,TacAlias(loc,s,l,tac)):raw_tactic_expr) in diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4 index 097f38f01d..aab672153d 100644 --- a/parsing/g_basevernac.ml4 +++ b/parsing/g_basevernac.ml4 @@ -424,7 +424,7 @@ GEXTEND Gram | -> None ]] ; grammar_tactic_rule: - [[ name = rule_name; "["; pil = LIST0 production_item; "]"; + [[ name = rule_name; "["; pil = LIST1 production_item; "]"; "->"; "["; t = Tactic.tactic; "]" -> (name, pil, t) ]] ; grammar_rule: diff --git a/parsing/g_vernacnew.ml4 b/parsing/g_vernacnew.ml4 index c21feb09e8..f839e8f212 100644 --- a/parsing/g_vernacnew.ml4 +++ b/parsing/g_vernacnew.ml4 @@ -694,7 +694,7 @@ GEXTEND Gram VernacNotation (local,c,Some(s,modl),None,sc) | IDENT "Tactic"; IDENT "Notation"; n = tactic_level; - pil = LIST0 production_item; ":="; t = Tactic.tactic + pil = LIST1 production_item; ":="; t = Tactic.tactic -> VernacTacticGrammar (n,["",pil,t]) | IDENT "Reserved"; IDENT "Notation"; local = locality; s = ne_string; diff --git a/parsing/tacextend.ml4 b/parsing/tacextend.ml4 index 3a20aad1b5..21b96c8a7f 100644 --- a/parsing/tacextend.ml4 +++ b/parsing/tacextend.ml4 @@ -267,8 +267,12 @@ EXTEND declare_tactic_v7 loc s l ] ] ; tacrule: - [ [ "["; l = LIST0 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" - -> (l,e) + [ [ "["; l = LIST1 tacargs; "]"; "->"; "["; e = Pcaml.expr; "]" + -> + if match List.hd l with TacNonTerm _ -> true | _ -> false then + (* En attendant la syntaxe de tacticielles *) + failwith "Tactic syntax must start with an identifier"; + (l,e) ] ] ; tacargs: |