1 files changed, 116 insertions, 135 deletions

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index da04d8786..d05e7d909 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -61,13 +61,13 @@ let explicitation_eq ex1 ex2 = match ex1, ex2 with
   Id.equal id1 id2
 | _ -> false
 
-let eq_located f (_, x) (_, y) = f x y
+let eq_ast f { CAst.v = x } { CAst.v = y } = f x y
 
 let rec cases_pattern_expr_eq p1 p2 =
   if CAst.(p1.v == p2.v) then true
   else match CAst.(p1.v, p2.v) with
   | CPatAlias(a1,i1), CPatAlias(a2,i2) ->
-      Id.equal i1 i2 && cases_pattern_expr_eq a1 a2
+      eq_ast Name.equal i1 i2 && cases_pattern_expr_eq a1 a2
   | CPatCstr(c1,a1,b1), CPatCstr(c2,a2,b2) ->
       eq_reference c1 c2 &&
       Option.equal (List.equal cases_pattern_expr_eq) a1 a2 &&
@@ -106,19 +106,19 @@ let rec constr_expr_eq e1 e2 =
   else match CAst.(e1.v, e2.v) with
     | CRef (r1,u1), CRef (r2,u2) -> eq_reference r1 r2 && eq_universes u1 u2
     | CFix(id1,fl1), CFix(id2,fl2) ->
-      eq_located Id.equal id1 id2 &&
+      eq_ast Id.equal id1 id2 &&
       List.equal fix_expr_eq fl1 fl2
     | CCoFix(id1,fl1), CCoFix(id2,fl2) ->
-      eq_located Id.equal id1 id2 &&
+      eq_ast Id.equal id1 id2 &&
       List.equal cofix_expr_eq fl1 fl2
     | CProdN(bl1,a1), CProdN(bl2,a2) ->
-      List.equal binder_expr_eq bl1 bl2 &&
+      List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
     | CLambdaN(bl1,a1), CLambdaN(bl2,a2) ->
-      List.equal binder_expr_eq bl1 bl2 &&
+      List.equal local_binder_eq bl1 bl2 &&
       constr_expr_eq a1 a2
-    | CLetIn((_,na1),a1,t1,b1), CLetIn((_,na2),a2,t2,b2) ->
-      Name.equal na1 na2 &&
+    | CLetIn(na1,a1,t1,b1), CLetIn(na2,a2,t2,b2) ->
+      eq_ast Name.equal na1 na2 &&
       constr_expr_eq a1 a2 &&
       Option.equal constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
@@ -141,14 +141,14 @@ let rec constr_expr_eq e1 e2 =
       List.equal case_expr_eq a1 a2 &&
       List.equal branch_expr_eq brl1 brl2
     | CLetTuple (n1, (m1, e1), t1, b1), CLetTuple (n2, (m2, e2), t2, b2) ->
-      List.equal (eq_located Name.equal) n1 n2 &&
-      Option.equal (eq_located Name.equal) m1 m2 &&
+      List.equal (eq_ast Name.equal) n1 n2 &&
+      Option.equal (eq_ast Name.equal) m1 m2 &&
       Option.equal constr_expr_eq e1 e2 &&
       constr_expr_eq t1 t2 &&
       constr_expr_eq b1 b2
     | CIf (e1, (n1, r1), t1, f1), CIf (e2, (n2, r2), t2, f2) ->
       constr_expr_eq e1 e2 &&
-      Option.equal (eq_located Name.equal) n1 n2 &&
+      Option.equal (eq_ast Name.equal) n1 n2 &&
       Option.equal constr_expr_eq r1 r2 &&
       constr_expr_eq t1 t2 &&
       constr_expr_eq f1 f2
@@ -181,32 +181,28 @@ let rec constr_expr_eq e1 e2 =
      | CGeneralization _ | CDelimiters _ | CProj _), _ -> false
 
 and args_eq (a1,e1) (a2,e2) =
-  Option.equal (eq_located explicitation_eq) e1 e2 &&
+  Option.equal (eq_ast explicitation_eq) e1 e2 &&
   constr_expr_eq a1 a2
 
 and case_expr_eq (e1, n1, p1) (e2, n2, p2) =
   constr_expr_eq e1 e2 &&
-  Option.equal (eq_located Name.equal) n1 n2 &&
+  Option.equal (eq_ast Name.equal) n1 n2 &&
   Option.equal cases_pattern_expr_eq p1 p2
 
-and branch_expr_eq (_, (p1, e1)) (_, (p2, e2)) =
+and branch_expr_eq {CAst.v=(p1, e1)} {CAst.v=(p2, e2)} =
   List.equal (List.equal cases_pattern_expr_eq) p1 p2 &&
   constr_expr_eq e1 e2
 
-and binder_expr_eq ((n1, _, e1) : binder_expr) (n2, _, e2) =
-  (** Don't care about the [binder_kind] *)
-  List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
-
 and fix_expr_eq (id1,(j1, r1),bl1,a1,b1) (id2,(j2, r2),bl2,a2,b2) =
-  (eq_located Id.equal id1 id2) &&
-  Option.equal (eq_located Id.equal) j1 j2 &&
+  (eq_ast Id.equal id1 id2) &&
+  Option.equal (eq_ast Id.equal) j1 j2 &&
   recursion_order_expr_eq r1 r2 &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
 
 and cofix_expr_eq (id1,bl1,a1,b1) (id2,bl2,a2,b2) =
-  (eq_located Id.equal id1 id2) &&
+  (eq_ast Id.equal id1 id2) &&
   List.equal local_binder_eq bl1 bl2 &&
   constr_expr_eq a1 a2 &&
   constr_expr_eq b1 b2
@@ -220,15 +216,16 @@ and recursion_order_expr_eq r1 r2 = match r1, r2 with
 
 and local_binder_eq l1 l2 = match l1, l2 with
   | CLocalDef (n1, e1, t1), CLocalDef (n2, e2, t2) ->
-    eq_located Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
+    eq_ast Name.equal n1 n2 && constr_expr_eq e1 e2 && Option.equal constr_expr_eq t1 t2
   | CLocalAssum (n1, _, e1), CLocalAssum (n2, _, e2) ->
     (** Don't care about the [binder_kind] *)
-    List.equal (eq_located Name.equal) n1 n2 && constr_expr_eq e1 e2
+    List.equal (eq_ast Name.equal) n1 n2 && constr_expr_eq e1 e2
   | _ -> false
 
-and constr_notation_substitution_eq (e1, el1, bl1) (e2, el2, bl2) =
+and constr_notation_substitution_eq (e1, el1, b1, bl1) (e2, el2, b2, bl2) =
   List.equal constr_expr_eq e1 e2 &&
   List.equal (List.equal constr_expr_eq) el1 el2 &&
+  List.equal cases_pattern_expr_eq b1 b2 &&
   List.equal (List.equal local_binder_eq) bl1 bl2
 
 and instance_eq (x1,c1) (x2,c2) =
@@ -247,12 +244,12 @@ and cast_expr_eq c1 c2 = match c1, c2 with
 let constr_loc c = CAst.(c.loc)
 let cases_pattern_expr_loc cp = CAst.(cp.loc)
 
-let local_binder_loc = function
-  | CLocalAssum ((loc,_)::_,_,t)
-  | CLocalDef ((loc,_),t,None) -> Loc.merge_opt loc (constr_loc t)
-  | CLocalDef ((loc,_),b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
+let local_binder_loc = let open CAst in function
+  | CLocalAssum ({ loc } ::_,_,t)
+  | CLocalDef ( { loc },t,None) -> Loc.merge_opt loc (constr_loc t)
+  | CLocalDef ( { loc },b,Some t) -> Loc.merge_opt loc (Loc.merge_opt (constr_loc b) (constr_loc t))
   | CLocalAssum ([],_,_) -> assert false
-  | CLocalPattern (loc,_) -> loc
+  | CLocalPattern { loc } -> loc
 
 let local_binders_loc bll = match bll with
   | []     -> None
@@ -260,9 +257,6 @@ let local_binders_loc bll = match bll with
 
 (** Folds and maps *)
 
-(* Legacy functions *)
-let down_located f (_l, x) = f x
-
 let is_constructor id =
   try Globnames.isConstructRef
         (Smartlocate.global_of_extended_global
@@ -272,7 +266,7 @@ let is_constructor id =
 let rec cases_pattern_fold_names f a pt = match CAst.(pt.v) with
   | CPatRecord l ->
     List.fold_left (fun acc (r, cp) -> cases_pattern_fold_names f acc cp) a l
-  | CPatAlias (pat,id) -> f id a
+  | CPatAlias (pat,{CAst.v=na}) -> Name.fold_right f na (cases_pattern_fold_names f a pat)
   | CPatOr (patl) ->
     List.fold_left (cases_pattern_fold_names f) a patl
   | CPatCstr (_,patl1,patl2) ->
@@ -304,25 +298,17 @@ let ids_of_cases_tomatch tms =
     (fun (_, ona, indnal) l ->
        Option.fold_right (fun t ids -> cases_pattern_fold_names Id.Set.add ids t)
          indnal
-         (Option.fold_right (down_located (Name.fold_right Id.Set.add)) ona l))
+         (Option.fold_right (CAst.with_val (Name.fold_right Id.Set.add)) ona l))
     tms Id.Set.empty
 
-let rec fold_constr_expr_binders g f n acc b = function
-  | (nal,bk,t)::l ->
-    let nal = snd (List.split nal) in
-    let n' = List.fold_right (Name.fold_right g) nal n in
-    f n (fold_constr_expr_binders g f n' acc b l) t
-  | [] ->
-    f n acc b
-
-let rec fold_local_binders g f n acc b = function
+let rec fold_local_binders g f n acc b = let open CAst in function
   | CLocalAssum (nal,bk,t)::l ->
-    let nal = snd (List.split nal) in
+    let nal = List.(map (fun {v} -> v) nal) in
     let n' = List.fold_right (Name.fold_right g) nal n in
     f n (fold_local_binders g f n' acc b l) t
-  | CLocalDef ((_,na),c,t)::l ->
+  | CLocalDef ( { v = na },c,t)::l ->
     Option.fold_left (f n) (f n (fold_local_binders g f (Name.fold_right g na n) acc b l) c) t
-  | CLocalPattern (_,(pat,t))::l ->
+  | CLocalPattern { v = pat,t }::l ->
     let acc = fold_local_binders g f (cases_pattern_fold_names g n pat) acc b l in
     Option.fold_left (f n) acc t
   | [] ->
@@ -331,12 +317,12 @@ let rec fold_local_binders g f n acc b = function
 let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
     | CAppExpl ((_,_,_),l) -> List.fold_left (f n) acc l
     | CApp ((_,t),l) -> List.fold_left (f n) (f n acc t) (List.map fst l)
-    | CProdN (l,b) | CLambdaN (l,b) -> fold_constr_expr_binders g f n acc b l
+    | CProdN (l,b) | CLambdaN (l,b) -> fold_local_binders g f n acc b l
     | CLetIn (na,a,t,b) ->
-      f (Name.fold_right g (snd na) n) (Option.fold_left (f n) (f n acc a) t) b
+      f (Name.fold_right g (na.CAst.v) n) (Option.fold_left (f n) (f n acc a) t) b
     | CCast (a,(CastConv b|CastVM b|CastNative b)) -> f n (f n acc a) b
     | CCast (a,CastCoerce) -> f n acc a
-    | CNotation (_,(l,ll,bll)) ->
+    | CNotation (_,(l,ll,bl,bll)) ->
       (* The following is an approximation: we don't know exactly if
          an ident is binding nor to which subterms bindings apply *)
       let acc = List.fold_left (f n) acc (l@List.flatten ll) in
@@ -350,18 +336,18 @@ let fold_constr_expr_with_binders g f n acc = CAst.with_val (function
       let ids = ids_of_cases_tomatch al in
       let acc = Option.fold_left (f (Id.Set.fold g ids n)) acc rtnpo in
       let acc = List.fold_left (f n) acc (List.map (fun (fst,_,_) -> fst) al) in
-      List.fold_right (fun (loc,(patl,rhs)) acc ->
+      List.fold_right (fun {CAst.v=(patl,rhs)} acc ->
           let ids = ids_of_pattern_list patl in
           f (Id.Set.fold g ids n) acc rhs) bl acc
     | CLetTuple (nal,(ona,po),b,c) ->
-      let n' = List.fold_right (down_located (Name.fold_right g)) nal n in
-      f (Option.fold_right (down_located (Name.fold_right g)) ona n') (f n acc b) c
+      let n' = List.fold_right (CAst.with_val (Name.fold_right g)) nal n in
+      f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n') (f n acc b) c
     | CIf (c,(ona,po),b1,b2) ->
       let acc = f n (f n (f n acc b1) b2) c in
       Option.fold_left
-        (f (Option.fold_right (down_located (Name.fold_right g)) ona n)) acc po
+        (f (Option.fold_right (CAst.with_val (Name.fold_right g)) ona n)) acc po
     | CFix (_,l) ->
-      let n' = List.fold_right (fun ((_,id),_,_,_,_) -> g id) l n in
+      let n' = List.fold_right (fun ( { CAst.v = id },_,_,_,_) -> g id) l n in
       List.fold_right (fun (_,(_,o),lb,t,c) acc ->
           fold_local_binders g f n'
             (fold_local_binders g f n acc t lb) c lb) l acc
@@ -380,24 +366,19 @@ let free_vars_of_constr_expr c =
 let occur_var_constr_expr id c = Id.Set.mem id (free_vars_of_constr_expr c)
 
 (* Used in correctness and interface *)
-let map_binder g e nal = List.fold_right (down_located (Name.fold_right g)) nal e
-
-let map_binders f g e bl =
-  (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
-  let h (e,bl) (nal,bk,t) = (map_binder g e nal,(nal,bk,f e t)::bl) in
-  let (e,rbl) = List.fold_left h (e,[]) bl in
-  (e, List.rev rbl)
+let map_binder g e nal = List.fold_right (CAst.with_val (Name.fold_right g)) nal e
 
 let map_local_binders f g e bl =
   (* TODO: avoid variable capture in [t] by some [na] in [List.tl nal] *)
+  let open CAst in
   let h (e,bl) = function
       CLocalAssum(nal,k,ty) ->
       (map_binder g e nal, CLocalAssum(nal,k,f e ty)::bl)
-    | CLocalDef((loc,na),c,ty) ->
-      (Name.fold_right g na e, CLocalDef((loc,na),f e c,Option.map (f e) ty)::bl)
-    | CLocalPattern (loc,(pat,t)) ->
+    | CLocalDef( { loc ; v = na } as cna ,c,ty) ->
+      (Name.fold_right g na e, CLocalDef(cna,f e c,Option.map (f e) ty)::bl)
+    | CLocalPattern { loc; v = pat,t } ->
       let ids = ids_of_pattern pat in
-      (Id.Set.fold g ids e, CLocalPattern (loc,(pat,Option.map (f e) t))::bl) in
+      (Id.Set.fold g ids e, CLocalPattern (make ?loc (pat,Option.map (f e) t))::bl) in
   let (e,rbl) = List.fold_left h (e,[]) bl in
   (e, List.rev rbl)
 
@@ -406,15 +387,15 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CApp ((p,a),l) ->
       CApp ((p,f e a),List.map (fun (a,i) -> (f e a,i)) l)
     | CProdN (bl,b) ->
-      let (e,bl) = map_binders f g e bl in CProdN (bl,f e b)
+      let (e,bl) = map_local_binders f g e bl in CProdN (bl,f e b)
     | CLambdaN (bl,b) ->
-      let (e,bl) = map_binders f g e bl in CLambdaN (bl,f e b)
+      let (e,bl) = map_local_binders f g e bl in CLambdaN (bl,f e b)
     | CLetIn (na,a,t,b) ->
-      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (snd na) e) b)
+      CLetIn (na,f e a,Option.map (f e) t,f (Name.fold_right g (na.CAst.v) e) b)
     | CCast (a,c) -> CCast (f e a, Miscops.map_cast_type (f e) c)
-    | CNotation (n,(l,ll,bll)) ->
+    | CNotation (n,(l,ll,bl,bll)) ->
       (* This is an approximation because we don't know what binds what *)
-      CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll,
+      CNotation (n,(List.map (f e) l,List.map (List.map (f e)) ll, bl,
                     List.map (fun bl -> snd (map_local_binders f g e bl)) bll))
     | CGeneralization (b,a,c) -> CGeneralization (b,a,f e c)
     | CDelimiters (s,a) -> CDelimiters (s,f e a)
@@ -422,32 +403,32 @@ let map_constr_expr_with_binders g f e = CAst.map (function
     | CPrim _ | CRef _ as x -> x
     | CRecord l -> CRecord (List.map (fun (id, c) -> (id, f e c)) l)
     | CCases (sty,rtnpo,a,bl) ->
-      let bl = List.map (fun (loc,(patl,rhs)) ->
+      let bl = List.map (fun {CAst.v=(patl,rhs);loc} ->
           let ids = ids_of_pattern_list patl in
-          (loc,(patl,f (Id.Set.fold g ids e) rhs))) bl in
+          CAst.make ?loc (patl,f (Id.Set.fold g ids e) rhs)) bl in
       let ids = ids_of_cases_tomatch a in
       let po = Option.map (f (Id.Set.fold g ids e)) rtnpo in
       CCases (sty, po, List.map (fun (tm,x,y) -> f e tm,x,y) a,bl)
     | CLetTuple (nal,(ona,po),b,c) ->
-      let e' = List.fold_right (down_located (Name.fold_right g)) nal e in
-      let e'' = Option.fold_right (down_located (Name.fold_right g)) ona e in
+      let e' = List.fold_right (CAst.with_val (Name.fold_right g)) nal e in
+      let e'' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
       CLetTuple (nal,(ona,Option.map (f e'') po),f e b,f e' c)
     | CIf (c,(ona,po),b1,b2) ->
-      let e' = Option.fold_right (down_located (Name.fold_right g)) ona e in
+      let e' = Option.fold_right (CAst.with_val (Name.fold_right g)) ona e in
       CIf (f e c,(ona,Option.map (f e') po),f e b1,f e b2)
     | CFix (id,dl) ->
       CFix (id,List.map (fun (id,n,bl,t,d) ->
           let (e',bl') = map_local_binders f g e bl in
           let t' = f e' t in
           (* Note: fix names should be inserted before the arguments... *)
-          let e'' = List.fold_left (fun e ((_,id),_,_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,n,bl',t',d')) dl)
     | CCoFix (id,dl) ->
       CCoFix (id,List.map (fun (id,bl,t,d) ->
           let (e',bl') = map_local_binders f g e bl in
           let t' = f e' t in
-          let e'' = List.fold_left (fun e ((_,id),_,_,_) -> g id e) e' dl in
+          let e'' = List.fold_left (fun e ({ CAst.v = id },_,_,_) -> g id e) e' dl in
           let d' = f e'' d in
           (id,bl',t',d')) dl)
     | CProj (p,c) ->
@@ -473,9 +454,10 @@ let locs_of_notation ?loc locs ntn =
     | (ba,ea)::l -> if Int.equal pos ba then aux ea l else (pos,ba)::aux ea l
   in aux bl (List.sort (fun l1 l2 -> fst l1 - fst l2) locs)
 
-let ntn_loc ?loc (args,argslist,binderslist) =
+let ntn_loc ?loc (args,argslist,binders,binderslist) =
   locs_of_notation ?loc
     (List.map constr_loc (args@List.flatten argslist)@
+     List.map cases_pattern_expr_loc binders@
      List.map local_binders_loc binderslist)
 
 let patntn_loc ?loc (args,argslist) =
@@ -487,17 +469,18 @@ let error_invalid_pattern_notation ?loc () =
 
 (* Interpret the index of a recursion order annotation *)
 let split_at_annot bl na =
-  let names = List.map snd (names_of_local_assums bl) in
+  let open CAst in
+  let names = List.map (fun { v } -> v) (names_of_local_assums bl) in
   match na with
   | None ->
     begin match names with
       | [] -> CErrors.user_err (Pp.str "A fixpoint needs at least one parameter.")
       | _ -> ([], bl)
     end
-  | Some (loc, id) ->
+  | Some { loc; v = id } ->
     let rec aux acc = function
       | CLocalAssum (bls, k, t) as x :: rest ->
-        let test (_, na) = match na with
+        let test { CAst.v = na } = match na with
           | Name id' -> Id.equal id id'
           | Anonymous -> false
         in
@@ -511,13 +494,13 @@ let split_at_annot bl na =
             in
             (List.rev ans, CLocalAssum (r, k, t) :: rest)
         end
-      | CLocalDef ((_,na),_,_) as x :: rest ->
+      | CLocalDef ({ CAst.v = na },_,_) as x :: rest ->
         if Name.equal (Name id) na then
           CErrors.user_err ?loc
             (Id.print id ++ str" must be a proper parameter and not a local definition.")
         else
           aux (x :: acc) rest
-      | CLocalPattern (_,_) :: rest ->
+      | CLocalPattern _ :: rest ->
         Loc.raise ?loc (Stream.Error "pattern with quote not allowed after fix")
       | [] ->
         CErrors.user_err ?loc
@@ -529,9 +512,9 @@ let split_at_annot bl na =
 let mkIdentC id   = CAst.make @@ CRef (Ident (Loc.tag id),None)
 let mkRefC r      = CAst.make @@ CRef (r,None)
 let mkCastC (a,k) = CAst.make @@ CCast (a,k)
-let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([idl,bk,a],b)
+let mkLambdaC (idl,bk,a,b) = CAst.make @@ CLambdaN ([CLocalAssum (idl,bk,a)],b)
 let mkLetInC  (id,a,t,b)   = CAst.make @@ CLetIn (id,a,t,b)
-let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([idl,bk,a],b)
+let mkProdC   (idl,bk,a,b) = CAst.make @@ CProdN ([CLocalAssum (idl,bk,a)],b)
 
 let mkAppC (f,l) =
   let l = List.map (fun x -> (x,None)) l in
@@ -539,56 +522,11 @@ let mkAppC (f,l) =
   | CApp (g,l') -> CAst.make @@ CApp (g, l' @ l)
   | _           -> CAst.make @@ CApp ((None, f), l)
 
-let add_name_in_env env n =
-  match snd n with
-  | Anonymous -> env
-  | Name id -> id :: env
-
-let fresh_var env c =
-  Namegen.next_ident_away (Id.of_string "pat")
-    (List.fold_left (fun accu id -> Id.Set.add id accu) (free_vars_of_constr_expr c) env)
-
-let expand_binders ?loc mkC bl c =
-  let rec loop ?loc bl c =
-    match bl with
-    | [] -> ([], c)
-    | b :: bl ->
-      match b with
-      | CLocalDef ((loc1,_) as n, oty, b) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let env = add_name_in_env env n in
-        (env, CAst.make ?loc @@ CLetIn (n,oty,b,c))
-      | CLocalAssum ((loc1,_)::_ as nl, bk, t) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let env = List.fold_left add_name_in_env env nl in
-        (env, mkC ?loc (nl,bk,t) c)
-      | CLocalAssum ([],_,_) -> loop ?loc bl c
-      | CLocalPattern (loc1, (p, ty)) ->
-        let env, c = loop ?loc:(Loc.merge_opt loc1 loc) bl c in
-        let ni = fresh_var env c in
-        let id = (loc1, Name ni) in
-        let ty = match ty with
-          | Some ty -> ty
-          | None -> CAst.make ?loc:loc1 @@ CHole (None, IntroAnonymous, None)
-        in
-        let e = CAst.make @@ CRef (Libnames.Ident (loc1, ni), None) in
-        let c = CAst.make ?loc @@
-          CCases
-            (LetPatternStyle, None, [(e,None,None)],
-             [(Loc.tag ?loc:loc1 ([[p]], c))])
-        in
-        (ni :: env, mkC ?loc ([id],Default Explicit,ty) c)
-  in
-  let (_, c) = loop ?loc bl c in
-  c
-
 let mkCProdN ?loc bll c =
-  let mk ?loc b c = CAst.make ?loc @@ CProdN ([b],c) in
-  expand_binders ?loc mk bll c
+  CAst.make ?loc @@ CProdN (bll,c)
 
 let mkCLambdaN ?loc bll c =
-  let mk ?loc b c = CAst.make ?loc @@ CLambdaN ([b],c) in
-  expand_binders ?loc mk bll c
+  CAst.make ?loc @@ CLambdaN (bll,c)
 
 let coerce_reference_to_id = function
   | Ident (_,id) -> id
@@ -597,17 +535,60 @@ let coerce_reference_to_id = function
       (str "This expression should be a simple identifier.")
 
 let coerce_to_id = function
-  | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,id)
+  | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc id
   | { CAst.loc; _ } -> CErrors.user_err ?loc
                          ~hdr:"coerce_to_id"
                          (str "This expression should be a simple identifier.")
 
 let coerce_to_name = function
-  | { CAst.v = CRef (Ident (loc,id),None) } -> (loc,Name id)
-  | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> (loc,Anonymous)
+  | { CAst.v = CRef (Ident (loc,id),None) } -> CAst.make ?loc @@ Name id
+  | { CAst.loc; CAst.v = CHole (None,Misctypes.IntroAnonymous,None) } -> CAst.make ?loc Anonymous
   | { CAst.loc; _ } -> CErrors.user_err ?loc ~hdr:"coerce_to_name"
                          (str "This expression should be a name.")
 
+let mkCPatOr ?loc = function
+  | [pat] -> pat
+  | disjpat -> CAst.make ?loc @@ (CPatOr disjpat)
+
+let mkAppPattern ?loc p lp =
+  let open CAst in
+  make ?loc @@ (match p.v with
+  | CPatAtom (Some r) -> CPatCstr (r, None, lp)
+  | CPatCstr (r, None, l2) ->
+     CErrors.user_err ?loc:p.loc ~hdr:"compound_pattern"
+                      (Pp.str "Nested applications not supported.")
+  | CPatCstr (r, l1, l2) -> CPatCstr (r, l1 , l2@lp)
+  | CPatNotation (n, s, l) -> CPatNotation (n , s, l@lp)
+  | _ -> CErrors.user_err
+           ?loc:p.loc ~hdr:"compound_pattern"
+           (Pp.str "Such pattern cannot have arguments."))
+
+let rec coerce_to_cases_pattern_expr c = CAst.map_with_loc (fun ?loc -> function
+  | CRef (r,None) ->
+     CPatAtom (Some r)
+  | CHole (None,Misctypes.IntroAnonymous,None) ->
+     CPatAtom None
+  | CLetIn ({CAst.loc;v=Name id},b,None,{ CAst.v = CRef (Ident (_,id'),None) }) when Id.equal id id' ->
+      CPatAlias (coerce_to_cases_pattern_expr b, CAst.(make ?loc @@ Name id))
+  | CApp ((None,p),args) when List.for_all (fun (_,e) -> e=None) args ->
+     (mkAppPattern (coerce_to_cases_pattern_expr p) (List.map (fun (a,_) -> coerce_to_cases_pattern_expr a) args)).CAst.v
+  | CAppExpl ((None,r,i),args) ->
+     CPatCstr (r,Some (List.map coerce_to_cases_pattern_expr args),[])
+  | CNotation (ntn,(c,cl,[],[])) ->
+     CPatNotation (ntn,(List.map coerce_to_cases_pattern_expr c,
+                        List.map (List.map coerce_to_cases_pattern_expr) cl),[])
+  | CPrim p ->
+     CPatPrim p
+  | CRecord l ->
+     CPatRecord (List.map (fun (r,p) -> (r,coerce_to_cases_pattern_expr p)) l)
+  | CDelimiters (s,p) ->
+     CPatDelimiters (s,coerce_to_cases_pattern_expr p)
+  | CCast (p,CastConv t) ->
+     CPatCast (coerce_to_cases_pattern_expr p,t)
+  | _ ->
+     CErrors.user_err ?loc ~hdr:"coerce_to_cases_pattern_expr"
+                      (str "This expression should be coercible to a pattern.")) c
+
 let asymmetric_patterns = ref (false)
 let _ = Goptions.declare_bool_option {
   Goptions.optdepr = false;