diff options
| author |  Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
|---|---|---|
| committer | Enrico Tassi <gareuselesinge@debian.org> | 2015-11-13 11:31:34 +0100 |
| commit | 2280477a96e19ba5060de2d48dcc8fd7c8079d22 (patch) | |
| tree | 074182834cb406d1304aec4233718564a9c06ba1 /grammar | |
| parent | 0aa2544d04dbd4b6ee665b551ed165e4fb02d2fa (diff) | |
Imported Upstream version 8.5~beta3+dfsg
Diffstat (limited to 'grammar')
| -rw-r--r-- | grammar/grammar.mllib | 5 | ||||
| -rw-r--r-- | grammar/tacextend.ml4 | 12 | ||||
| -rw-r--r-- | grammar/vernacextend.ml4 | 2 |
3 files changed, 13 insertions, 6 deletions
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 0b168377..60ea0df0 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,6 +1,7 @@ Coq_config Hook +Terminal Canary Hashset Hashcons @@ -19,12 +20,14 @@ Serialize Stateid Feedback Pp -Errors + CList CString CArray CStack Util +Ppstyle +Errors Bigint Predicate Segmenttree diff --git a/grammar/tacextend.ml4 b/grammar/tacextend.ml4 index 0421ad7c..66f82fcd 100644 --- a/grammar/tacextend.ml4 +++ b/grammar/tacextend.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +(** Implementation of the TACTIC EXTEND macro. *) + open Util open Pp open Names @@ -172,17 +174,17 @@ let is_constr_gram = function | Aentry ("constr", "constr") -> true | _ -> false -let make_vars len = - (** We choose names unlikely to be written by a human, even though that - does not matter at all. *) - List.init len (fun i -> Some (Id.of_string (Printf.sprintf "_%i" i))) +let make_var = function + | GramNonTerminal(loc',_,_,Some p) -> Some p + | GramNonTerminal(loc',_,_,None) -> Some (Id.of_string "_") + | _ -> assert false let declare_tactic loc s c cl = match cl with | [(GramTerminal name) :: rem, _, tac] when List.for_all is_constr_gram rem -> (** The extension is only made of a name followed by constr entries: we do not add any grammar nor printing rule and add it as a true Ltac definition. *) let patt = make_patt rem in - let vars = make_vars (List.length rem) in + let vars = List.map make_var rem in let vars = mlexpr_of_list (mlexpr_of_option mlexpr_of_ident) vars in let entry = mlexpr_of_string s in let se = <:expr< { Tacexpr.mltac_tactic = $entry$; Tacexpr.mltac_plugin = $plugin_name$ } >> in diff --git a/grammar/vernacextend.ml4 b/grammar/vernacextend.ml4 index 9db89308..03061d8b 100644 --- a/grammar/vernacextend.ml4 +++ b/grammar/vernacextend.ml4 @@ -8,6 +8,8 @@ (*i camlp4deps: "tools/compat5b.cmo" i*) +(** Implementation of the VERNAC EXTEND macro. *) + open Pp open Util open Q_util |