diff options
| author | herbelin | 2005-05-17 13:23:34 +0000 |
|---|---|---|
| committer | herbelin | 2005-05-17 13:23:34 +0000 |
| commit | 0d25cb99daa91fdc3b2ceedc87c6c1480e8577b6 (patch) | |
| tree | a79a78a20cd7a608e773bf4e4ee2c1229b895a2e | |
| parent | ddc83ed89cd6671cfa6b5bf2d0ce1fb74ad206c1 (diff) | |
Affinements suite à extension Tactic Notation aux tacticielles
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7030 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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: |