diff options
| author | Hugo Herbelin | 2018-10-08 17:46:09 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-10-08 20:42:14 +0200 |
| commit | ab237af7e952281e3fe695d888242cdf2abcaa90 (patch) | |
| tree | bcdb9c257db9ada14dac7b5f5d43fd26eef0e1da /interp/notation_ops.ml | |
| parent | d792c2bf18e68a6301f295c79c05f25738456ecf (diff) | |
Fixes #8672 (ill-formed pattern substitution in notation with "let").
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index ff5e2bb5f3..ab57176643 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -153,11 +153,13 @@ let protect g e na = if disjpat <> None then user_err (Pp.str "Unsupported substitution of an arbitrary pattern."); e',na -let apply_cases_pattern ?loc ((ids,disjpat),id) c = - let tm = DAst.make ?loc (GVar id) in +let apply_cases_pattern_term ?loc (ids,disjpat) tm c = let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in DAst.make ?loc @@ GCases (Constr.LetPatternStyle, None, [tm,(Anonymous,None)], eqns) +let apply_cases_pattern ?loc (ids_disjpat,id) c = + apply_cases_pattern_term ?loc ids_disjpat (DAst.make ?loc (GVar id)) c + let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let lt x = DAst.make ?loc x in lt @@ match nc with | NVar id -> GVar id @@ -182,7 +184,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = let e',disjpat,na = g e na in (match disjpat with | None -> GLetIn (na,f e b,Option.map (f e) t,f e' c) - | Some disjpat -> DAst.get (apply_cases_pattern ?loc disjpat (f e' c))) + | Some (disjpat,_id) -> DAst.get (apply_cases_pattern_term ?loc disjpat (f e b) (f e' c))) | NCases (sty,rtntypopt,tml,eqnl) -> let e',tml' = List.fold_right (fun (tm,(na,t)) (e',tml') -> let e',t' = match t with |