From ab237af7e952281e3fe695d888242cdf2abcaa90 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Mon, 8 Oct 2018 17:46:09 +0200
Subject: Fixes #8672 (ill-formed pattern substitution in notation with "let").

---
 interp/notation_ops.ml | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

(limited to 'interp/notation_ops.ml')

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
-- 
cgit v1.2.3