summaryrefslogtreecommitdiff
path: root/interp/constrextern.ml
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:44:20 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2011-04-19 16:44:20 +0200
commit9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch)
treea418d1edb3d53cdb4185b9719b7a70822cf5a24d /interp/constrextern.ml
parent6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff)
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r--interp/constrextern.ml27
1 files changed, 15 insertions, 12 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index fd230539..1716cfad 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: constrextern.ml 13492 2010-10-04 21:20:01Z herbelin $ *)
+(* $Id: constrextern.ml 13967 2011-04-08 14:08:43Z herbelin $ *)
(*i*)
open Pp
@@ -343,6 +343,10 @@ let make_pat_notation loc ntn (terms,termlists as subst) =
(fun (loc,p) -> CPatPrim (loc,p))
destPatPrim terms
+let mkPat loc qid l =
+ (* Normally irrelevant test with v8 syntax, but let's do it anyway *)
+ if l = [] then CPatAtom (loc,Some qid) else CPatCstr (loc,qid,l)
+
(* Better to use extern_rawconstr composed with injection/retraction ?? *)
let rec extern_cases_pattern_in_scope (scopes:local_scopes) vars pat =
try
@@ -397,15 +401,9 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
(match keyrule with
| NotationRule (sc,ntn) -> raise No_match
| SynDefRule kn ->
- let p =
- let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
- if l = [] then
- CPatAtom (loc,Some qid)
- else
- let l =
- List.map (extern_cases_pattern_in_scope allscopes vars) l in
- CPatCstr (loc,qid,l) in
- insert_pat_alias loc p na)
+ let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+ let l = List.map (extern_cases_pattern_in_scope allscopes vars) l in
+ insert_pat_alias loc (mkPat loc qid l) na)
| PatCstr (_,f,l,_), Some n when List.length l > n ->
raise No_match
| PatCstr (loc,_,_,na),_ ->
@@ -432,8 +430,13 @@ and extern_symbol_pattern (tmp_scope,scopes as allscopes) vars t = function
insert_pat_delimiters loc
(make_pat_notation loc ntn (l,ll)) key)
| SynDefRule kn ->
- let qid = shortest_qualid_of_syndef vars kn in
- CPatAtom (loc,Some (Qualid (loc, qid))) in
+ let qid = Qualid (loc, shortest_qualid_of_syndef vars kn) in
+ let l =
+ List.map (fun (c,(scopt,scl)) ->
+ extern_cases_pattern_in_scope (scopt,scl@scopes) vars c)
+ subst in
+ assert (substlist = []);
+ mkPat loc qid l in
insert_pat_alias loc p na
| PatVar (loc,Anonymous),_ -> CPatAtom (loc, None)
| PatVar (loc,Name id),_ -> CPatAtom (loc, Some (Ident (loc,id)))