diff options
author | 2011-04-19 16:44:20 +0200 | |
---|---|---|
committer | 2011-04-19 16:44:20 +0200 | |
commit | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (patch) | |
tree | a418d1edb3d53cdb4185b9719b7a70822cf5a24d /interp/constrextern.ml | |
parent | 6b691bbd2101fd39395c0d2135fd7c06a8915e14 (diff) |
Imported Upstream version 8.3.pl2upstream/8.3.pl2
Diffstat (limited to 'interp/constrextern.ml')
-rw-r--r-- | interp/constrextern.ml | 27 |
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))) |