diff options
Diffstat (limited to 'parsing/egrammar.ml')
| -rw-r--r-- | parsing/egrammar.ml | 9 |
1 files changed, 7 insertions, 2 deletions
diff --git a/parsing/egrammar.ml b/parsing/egrammar.ml index 397189271..60848fdfd 100644 --- a/parsing/egrammar.ml +++ b/parsing/egrammar.ml @@ -284,12 +284,17 @@ let subst_constr_expr a loc subs = | CDelimiters (_,s,a) -> CDelimiters (loc,s,subst a) | CHole _ | CEvar _ | CPatVar _ | CSort _ | CNumeral _ | CDynamic _ | CRef _ as x -> x - | CCases (_,po,a,bl) -> + | CCases (_,(po,rtntypo),a,bl) -> (* TODO: apply g on the binding variables in pat... *) let bl = List.map (fun (_,pat,rhs) -> (loc,pat,subst rhs)) bl in - CCases (loc,option_app subst po,List.map subst a,bl) + CCases (loc,(option_app subst po,option_app subst rtntypo), + List.map (fun (tm,x) -> subst tm,x) a,bl) | COrderedCase (_,s,po,a,bl) -> COrderedCase (loc,s,option_app subst po,subst a,List.map subst bl) + | CLetTuple (_,nal,(na,po),a,b) -> + let na = name_app (subst_id subs) na in + let nal = List.map (name_app (subst_id subs)) nal in + CLetTuple (loc,nal,(na,option_app subst po),subst a,subst b) | CFix (_,id,dl) -> CFix (loc,id,List.map (fun (id,n,t,d) -> (id,n,subst t,subst d)) dl) | CCoFix (_,id,dl) -> |