diff options
Diffstat (limited to 'parsing/pcoq.ml4')
| -rw-r--r-- | parsing/pcoq.ml4 | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index 39047e688..476b3abd5 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -353,6 +353,8 @@ module Constr = let pattern = Gram.Entry.create "constr:pattern" let annot = Gram.Entry.create "constr:annot" let constr_pattern = gec_constr "constr_pattern" + let binder_let = Gram.Entry.create "constr:binder_list" + let tuple_constr = Gram.Entry.create "constr:tuple_constr" end module Module = @@ -618,6 +620,11 @@ let get_constr_entry en = snd (get_entry (get_univ "constr") "binder_constr"), None, false + | ETConstr(250,()) when not !Options.v7 -> + weaken_entry Constr.tuple_constr, +(* snd (get_entry (get_univ "constr") "tuple_construple"),*) + None, + false | _ -> compute_entry true (fun (n,()) -> Some n) en (* This computes the name to give to a production knowing the name and |