diff options
| author | herbelin | 2003-09-21 22:49:35 +0000 |
|---|---|---|
| committer | herbelin | 2003-09-21 22:49:35 +0000 |
| commit | a1fd83954be09cf9df9ba33c92bf4f7d1f733add (patch) | |
| tree | e125b950ba940bb14d79ba1fadbf277769942231 | |
| parent | c6417ebc8a670d69bff628a15e0ae0a8d43b8091 (diff) | |
Parsing au niveau lconstr des patterns de 'match context'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4432 85f007b7-540e-0410-9357-904b9bb8a0f7
| -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 ed66640353..672aeb3b64 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 b3cad569f5..46561d2cd2 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 a591f57b26..8f393030ed 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 |