diff options
| -rw-r--r-- | parsing/g_ltacnew.ml4 | 6 | ||||
| -rw-r--r-- | parsing/pcoq.ml4 | 3 | ||||
| -rw-r--r-- | parsing/pcoq.mli | 1 |
3 files changed, 6 insertions, 4 deletions
diff --git a/parsing/g_ltacnew.ml4 b/parsing/g_ltacnew.ml4 index ed6664035..672aeb3b6 100644 --- a/parsing/g_ltacnew.ml4 +++ b/parsing/g_ltacnew.ml4 @@ -160,10 +160,10 @@ GEXTEND Gram (name,(it,body)) ] ] ; match_pattern: - [ [ id = Constr.constr_pattern; "["; pc = Constr.constr_pattern; "]" -> + [ [ id = Constr.lconstr_pattern; "["; pc = Constr.lconstr_pattern; "]" -> let s = coerce_to_id id in Subterm (Some s, pc) - | "["; pc = Constr.constr_pattern; "]" -> Subterm (None,pc) - | pc = Constr.constr_pattern -> Term pc ] ] + | "["; pc = Constr.lconstr_pattern; "]" -> Subterm (None,pc) + | pc = Constr.lconstr_pattern -> Term pc ] ] ; match_hyps: [ [ na = name; ":"; mp = match_pattern -> Hyp (na, mp) ] ] diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4 index b3cad569f..46561d2cd 100644 --- a/parsing/pcoq.ml4 +++ b/parsing/pcoq.ml4 @@ -353,6 +353,7 @@ module Constr = let pattern = Gram.Entry.create "constr:pattern" let annot = Gram.Entry.create "constr:annot" let constr_pattern = gec_constr "constr_pattern" + let lconstr_pattern = gec_constr "lconstr_pattern" let binder_let = Gram.Entry.create "constr:binder_list" let tuple_constr = gec_constr "tuple_constr" end @@ -409,7 +410,7 @@ let reset_all_grammars () = let f = Gram.Unsafe.clear_entry in List.iter f [Constr.constr;Constr.operconstr;Constr.lconstr;Constr.annot; - Constr.constr_pattern]; + Constr.constr_pattern;Constr.lconstr_pattern]; f Constr.ident; f Constr.global; f Constr.sort; f Constr.pattern; f Module.module_expr; f Module.module_type; f Tactic.simple_tactic; diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index a591f57b2..8f393030e 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -138,6 +138,7 @@ module Constr : val pattern : cases_pattern_expr Gram.Entry.e val annot : constr_expr Gram.Entry.e val constr_pattern : constr_expr Gram.Entry.e + val lconstr_pattern : constr_expr Gram.Entry.e val binder_let : local_binder Gram.Entry.e val tuple_constr : constr_expr Gram.Entry.e end |