Making detyping potentially lazy.

The internal detype function takes an additional arguments dictating
whether it should be eager or lazy.

We introduce a new type of delayed `DAst.t` AST nodes and use it for
`glob_constr`.

Such type, instead of only containing a value, it can contain a lazy
computation too. We use a GADT to discriminate between both uses
statically, so that no delayed terms ever happen to be
marshalled (which would raise anomalies).

We also fix a regression in the test-suite:

  Mixing laziness and effects is a well-known hell. Here, an exception
  that was raised for mere control purpose was delayed and raised at a
  later time as an anomaly. We make the offending function eager.

1 files changed, 154 insertions, 112 deletions

diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 565a7e642..034116731 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -99,43 +99,43 @@ let name_to_ident = function
 
 let to_id g e id = let e,na = g e (Name id) in e,name_to_ident na
 
-let rec cases_pattern_fold_map ?loc g e = CAst.with_val (function
+let rec cases_pattern_fold_map ?loc g e = DAst.with_val (function
   | PatVar na ->
-      let e',na' = g e na in e', CAst.make ?loc @@ PatVar na'
+      let e',na' = g e na in e', DAst.make ?loc @@ PatVar na'
   | PatCstr (cstr,patl,na) ->
       let e',na' = g e na in
       let e',patl' = List.fold_left_map (cases_pattern_fold_map ?loc g) e patl in
-      e', CAst.make ?loc @@ PatCstr (cstr,patl',na')
+      e', DAst.make ?loc @@ PatCstr (cstr,patl',na')
   )
 
 let subst_binder_type_vars l = function
   | Evar_kinds.BinderType (Name id) ->
      let id =
-       try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
+       try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
        with Not_found -> id in
      Evar_kinds.BinderType (Name id)
   | e -> e
 
-let rec subst_glob_vars l gc = CAst.map (function
-  | GVar id as r -> (try (Id.List.assoc id l).CAst.v with Not_found -> r)
+let rec subst_glob_vars l gc = DAst.map (function
+  | GVar id as r -> (try DAst.get (Id.List.assoc id l) with Not_found -> r)
   | GProd (Name id,bk,t,c) ->
       let id =
-	try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
+	try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
 	with Not_found -> id in
       GProd (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
   | GLambda (Name id,bk,t,c) ->
       let id =
-	try match Id.List.assoc id l with { CAst.v = GVar id' } -> id' | _ -> id
+	try match DAst.get (Id.List.assoc id l) with GVar id' -> id' | _ -> id
 	with Not_found -> id in
       GLambda (Name id,bk,subst_glob_vars l t,subst_glob_vars l c)
   | GHole (x,naming,arg) -> GHole (subst_binder_type_vars l x,naming,arg)
-  | _ -> (map_glob_constr (subst_glob_vars l) gc).CAst.v (* assume: id is not binding *)
+  | _ -> DAst.get (map_glob_constr (subst_glob_vars l) gc) (* assume: id is not binding *)
   ) gc
 
 let ldots_var = Id.of_string ".."
 
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
-  let lt x = CAst.make ?loc x in lt @@ match nc with
+  let lt x = DAst.make ?loc x in lt @@ match nc with
   | NVar id -> GVar id
   | NApp (a,args) -> GApp (f e a, List.map (f e) args)
   | NList (x,y,iter,tail,swap) ->
@@ -143,13 +143,13 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
       let innerl = (ldots_var,t)::(if swap then [] else [x, lt @@ GVar y]) in
       let inner  = lt @@ GApp (lt @@ GVar (ldots_var),[subst_glob_vars innerl it]) in
       let outerl = (ldots_var,inner)::(if swap then [x, lt @@ GVar y] else []) in
-      (subst_glob_vars outerl it).CAst.v
+      DAst.get (subst_glob_vars outerl it)
   | NBinderList (x,y,iter,tail) ->
       let t = f e tail in let it = f e iter in
       let innerl = [(ldots_var,t);(x, lt @@ GVar y)] in
       let inner  = lt @@ GApp (lt @@ GVar ldots_var,[subst_glob_vars innerl it]) in
       let outerl = [(ldots_var,inner)] in
-      (subst_glob_vars outerl it).CAst.v
+      DAst.get (subst_glob_vars outerl it)
   | NLambda (na,ty,c) ->
       let e',na = g e na in GLambda (na,Explicit,f e ty,f e' c)
   | NProd (na,ty,c) ->
@@ -201,28 +201,34 @@ let glob_constr_of_notation_constr ?loc x =
 let add_id r id = r := (id :: pi1 !r, pi2 !r, pi3 !r)
 let add_name r = function Anonymous -> () | Name id -> add_id r id
 
+let is_gvar id c = match DAst.get c with
+| GVar id' -> Id.equal id id'
+| _ -> false
+
 let split_at_recursive_part c =
   let sub = ref None in
-  let open CAst in
-  let rec aux = function
-  | { loc = loc0; v = GApp ({ loc; v = GVar v },c::l) } when Id.equal v ldots_var -> (*  *)
+  let rec aux c =
+    let loc0 = c.CAst.loc in
+    match DAst.get c with
+    | GApp (f, c::l) when is_gvar ldots_var f -> (*  *)
+      let loc = f.CAst.loc in
       begin match !sub with
       | None ->
         let () = sub := Some c in
         begin match l with
-        | []     -> CAst.make ?loc @@ GVar ldots_var
-        | _ :: _ -> CAst.make ?loc:loc0 @@ GApp (CAst.make ?loc @@ GVar ldots_var, l)
+        | []     -> DAst.make ?loc @@ GVar ldots_var
+        | _ :: _ -> DAst.make ?loc:loc0 @@ GApp (DAst.make ?loc @@ GVar ldots_var, l)
         end
       | Some _ ->
         (* Not narrowed enough to find only one recursive part *)
         raise Not_found
       end
-  | c -> map_glob_constr aux c in
+    | _ -> map_glob_constr aux c in
   let outer_iterator = aux c in
   match !sub with
   | None -> (* No recursive pattern found *) raise Not_found
   | Some c ->
-  match outer_iterator.v with
+  match DAst.get outer_iterator with
   | GVar v when Id.equal v ldots_var -> (* Not enough context *) raise Not_found
   | _ -> outer_iterator, c
 
@@ -231,7 +237,7 @@ let subtract_loc loc1 loc2 =
   let l2 = fst (Option.cata Loc.unloc (0,0) loc2) in
   Some (Loc.make_loc (l1,l2-1))
 
-let check_is_hole id = function { CAst.v = GHole _ } -> () | t ->
+let check_is_hole id t = match DAst.get t with GHole _ -> () | _ ->
   user_err ?loc:(loc_of_glob_constr t)
    (strbrk "In recursive notation with binders, " ++ pr_id id ++
     strbrk " is expected to come without type.")
@@ -243,21 +249,24 @@ type recursive_pattern_kind =
 | RecursiveBinders of glob_constr * glob_constr
 
 let compare_recursive_parts found f f' (iterator,subc) =
-  let open CAst in
   let diff = ref None in
   let terminator = ref None in
-  let rec aux c1 c2 = match c1.v, c2.v with
+  let rec aux c1 c2 = match DAst.get c1, DAst.get c2 with
   | GVar v, term when Id.equal v ldots_var ->
       (* We found the pattern *)
       assert (match !terminator with None -> true | Some _ -> false);
       terminator := Some c2;
       true
-  | GApp ({ v = GVar v },l1), GApp (term, l2) when Id.equal v ldots_var ->
+  | GApp (f,l1), GApp (term, l2) ->
+    begin match DAst.get f with
+    | GVar v when Id.equal v ldots_var ->
       (* We found the pattern, but there are extra arguments *)
       (* (this allows e.g. alternative (recursive) notation of application) *)
       assert (match !terminator with None -> true | Some _ -> false);
       terminator := Some term;
       List.for_all2eq aux l1 l2
+    | _ -> mk_glob_constr_eq aux c1 c2
+    end
   | GVar x, GVar y when not (Id.equal x y) ->
       (* We found the position where it differs *)
       let lassoc = match !terminator with None -> false | Some _ -> true in
@@ -301,13 +310,13 @@ let compare_recursive_parts found f f' (iterator,subc) =
             (pi1 !found, (x,y) :: pi2 !found, pi3 !found),x,y,lassoc in
 	let iterator =
 	  f' (if lassoc then iterator
-	      else subst_glob_vars [x, CAst.make @@ GVar y] iterator) in
+	      else subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	NList (x,y,iterator,f (Option.get !terminator),lassoc)
     | Some (x,y,RecursiveBinders (t_x,t_y)) ->
 	let newfound = (pi1 !found, pi2 !found, (x,y) :: pi3 !found) in
-	let iterator = f' (subst_glob_vars [x, CAst.make @@ GVar y] iterator) in
+	let iterator = f' (subst_glob_vars [x, DAst.make @@ GVar y] iterator) in
 	(* found have been collected by compare_constr *)
 	found := newfound;
 	check_is_hole x t_x;
@@ -325,15 +334,20 @@ let notation_constr_and_vars_of_glob_constr a =
     try compare_recursive_parts found aux aux' (split_at_recursive_part c)
     with Not_found ->
     found := keepfound;
-    match c.CAst.v with
-    | GApp ({ CAst.v = GVar f; loc},[c]) when Id.equal f ldots_var ->
+    match DAst.get c with
+    | GApp (t, [_]) ->
+      begin match DAst.get t with
+      | GVar f when Id.equal f ldots_var ->
 	(* Fall on the second part of the recursive pattern w/o having
 	   found the first part *)
+        let loc = t.CAst.loc in
 	user_err ?loc 
 	(str "Cannot find where the recursive pattern starts.")
+      | _ -> aux' c
+      end
     | _c ->
 	aux' c
-  and aux' x = CAst.with_val (function
+  and aux' x = DAst.with_val (function
   | GVar id -> add_id found id; NVar id
   | GApp (g,args) -> NApp (aux g, List.map aux args)
   | GLambda (na,bk,ty,c) -> add_name found na; NLambda (na,aux ty,aux c)
@@ -433,7 +447,7 @@ let notation_constr_of_glob_constr nenv a =
 
 let notation_constr_of_constr avoiding t =
   let t = EConstr.of_constr t in
-  let t = Detyping.detype false avoiding (Global.env()) Evd.empty t in
+  let t = Detyping.detype Detyping.Now false avoiding (Global.env()) Evd.empty t in
   let nenv = {
     ninterp_var_type = Id.Map.empty;
     ninterp_rec_vars = Id.Map.empty;
@@ -441,13 +455,13 @@ let notation_constr_of_constr avoiding t =
   notation_constr_of_glob_constr nenv t
 
 let rec subst_pat subst pat =
-  match pat.CAst.v with
+  match DAst.get pat with
   | PatVar _ -> pat
   | PatCstr (((kn,i),j),cpl,n) ->
       let kn' = subst_mind subst kn
       and cpl' = List.smartmap (subst_pat subst) cpl in
       if kn' == kn && cpl' == cpl then pat else
-        CAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
+        DAst.make ?loc:pat.CAst.loc @@ PatCstr (((kn',i),j),cpl',n)
 
 let rec subst_notation_constr subst bound raw =
   match raw with
@@ -576,14 +590,14 @@ let abstract_return_type_context pi mklam tml rtno =
     List.fold_right mklam nal rtn)
     rtno
 
-let abstract_return_type_context_glob_constr =
+let abstract_return_type_context_glob_constr tml rtn =
   abstract_return_type_context (fun (_,(_,nal)) -> nal)
-    (fun na c -> CAst.make @@
-      GLambda(na,Explicit,CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c))
+    (fun na c -> DAst.make @@
+      GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn
 
-let abstract_return_type_context_notation_constr =
+let abstract_return_type_context_notation_constr tml rtn =
   abstract_return_type_context snd
-    (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c))
+    (fun na c -> NLambda(na,NHole (Evar_kinds.InternalHole, Misctypes.IntroAnonymous, None),c)) tml rtn
 
 let is_term_meta id metas =
   try match Id.List.assoc id metas with _,(NtnTypeConstr | NtnTypeConstrList) -> true | _ -> false
@@ -651,19 +665,23 @@ let add_binding_env alp (terms,onlybinders,termlists,binderlists) var v =
 let add_bindinglist_env (terms,onlybinders,termlists,binderlists) x bl =
   (terms,onlybinders,termlists,(x,bl)::binderlists)
 
-let rec pat_binder_of_term t = CAst.map (function
+let rec pat_binder_of_term t = DAst.map (function
   | GVar id -> PatVar (Name id)
-  | GApp ({ CAst.v = GRef (ConstructRef cstr,_)}, l) ->
+  | GApp (t, l) ->
+    begin match DAst.get t with
+    | GRef (ConstructRef cstr,_) ->
      let nparams = Inductiveops.inductive_nparams (fst cstr) in
      let _,l = List.chop nparams l in
      PatCstr (cstr, List.map pat_binder_of_term l, Anonymous)
+    | _ -> raise No_match
+    end
   | _ -> raise No_match
   ) t
 
 let bind_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var v =
   try
     let v' = Id.List.assoc var terms in
-    match CAst.(v.v, v'.v) with
+    match DAst.get v, DAst.get v' with
     | GHole _, _ -> sigma
     | _, GHole _ ->
         let sigma = Id.List.remove_assoc var terms,onlybinders,termlists,binderlists in
@@ -677,7 +695,7 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var
   try
     let vl' = Id.List.assoc var termlists in
     let unify_term v v' =
-      match CAst.(v.v, v'.v) with
+      match DAst.get v, DAst.get v' with
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v' else raise No_match in
@@ -693,8 +711,8 @@ let bind_termlist_env alp (terms,onlybinders,termlists,binderlists as sigma) var
 
 let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
   try
-    match Id.List.assoc var terms with
-    | { CAst.v = GVar id' } ->
+    match DAst.get (Id.List.assoc var terms) with
+    | GVar id' ->
        (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp),
        sigma
     | _ -> anomaly (str "A term which can be a binder has to be a variable.")
@@ -702,7 +720,7 @@ let bind_term_as_binding_env alp (terms,onlybinders,termlists,binderlists as sig
     (* The matching against a term allowing to find the instance has not been found yet *)
     (* If it will be a different name, we shall unfortunately fail *)
     (* TODO: look at the consequences for alp *)
-    alp, add_env alp sigma var (CAst.make @@ GVar id)
+    alp, add_env alp sigma var (DAst.make @@ GVar id)
 
 let bind_binding_as_term_env alp (terms,onlybinders,termlists,binderlists as sigma) var id =
   try
@@ -729,17 +747,19 @@ let bind_binding_env alp (terms,onlybinders,termlists,binderlists as sigma) var
         else (fst alp,(id1,id2)::snd alp),sigma
   with Not_found -> alp, add_binding_env alp sigma var v
 
-let rec map_cases_pattern_name_left f = CAst.map (function
+let rec map_cases_pattern_name_left f = DAst.map (function
   | PatVar na -> PatVar (f na)
   | PatCstr (c,l,na) -> PatCstr (c,List.map_left (map_cases_pattern_name_left f) l,f na)
   )
 
-let rec fold_cases_pattern_eq f x p p' = let open CAst in match p, p' with
-  | { loc; v = PatVar na}, { v = PatVar na' } -> let x,na = f x na na' in x, CAst.make ?loc @@ PatVar na
-  | { loc; v = PatCstr (c,l,na)}, { v = PatCstr (c',l',na') } when eq_constructor c c' ->
+let rec fold_cases_pattern_eq f x p p' =
+  let loc = p.CAst.loc in
+  match DAst.get p, DAst.get p' with
+  | PatVar na, PatVar na' -> let x,na = f x na na' in x, DAst.make ?loc @@ PatVar na
+  | PatCstr (c,l,na), PatCstr (c',l',na') when eq_constructor c c' ->
      let x,l = fold_cases_pattern_list_eq f x l l' in
      let x,na = f x na na' in
-     x, CAst.make ?loc @@ PatCstr (c,l,na)
+     x, DAst.make ?loc @@ PatCstr (c,l,na)
   | _ -> failwith "Not equal"
 
 and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
@@ -750,7 +770,7 @@ and fold_cases_pattern_list_eq f x pl pl' = match pl, pl' with
      x, p :: pl
   | _ -> assert false
 
-let rec cases_pattern_eq p1 p2 = match CAst.(p1.v, p2.v) with
+let rec cases_pattern_eq p1 p2 = match DAst.get p1, DAst.get p2 with
 | PatVar na1, PatVar na2 -> Name.equal na1 na2
 | PatCstr (c1, pl1, na1), PatCstr (c2, pl2, na2) ->
   eq_constructor c1 c2 && List.equal cases_pattern_eq pl1 pl2 &&
@@ -771,7 +791,7 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
     let unify_pat alp p p' =
       try fold_cases_pattern_eq unify_name alp p p' with Failure _ -> raise No_match in
     let unify_term alp v v' =
-      match CAst.(v.v, v'.v) with
+      match DAst.get v, DAst.get v' with
       | GHole _, _ -> v'
       | _, GHole _ -> v
       | _, _ -> if glob_constr_eq (alpha_rename (snd alp) v) v' then v else raise No_match in
@@ -783,16 +803,16 @@ let bind_bindinglist_env alp (terms,onlybinders,termlists,binderlists as sigma)
     let unify_binding_kind bk bk' = if bk == bk' then bk' else raise No_match in
     let unify_binder alp b b' =
       let loc, loc' = CAst.(b.loc, b'.loc) in
-      match CAst.(b.v, b'.v) with
+      match DAst.get b, DAst.get b' with
       | GLocalAssum (na,bk,t), GLocalAssum (na',bk',t') ->
          let alp, na = unify_name alp na na' in
-         alp, CAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
+         alp, DAst.make ?loc @@ GLocalAssum (na, unify_binding_kind bk bk', unify_term alp t t')
       | GLocalDef (na,bk,c,t), GLocalDef (na',bk',c',t') ->
          let alp, na = unify_name alp na na' in
-         alp, CAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
+         alp, DAst.make ?loc @@ GLocalDef (na, unify_binding_kind bk bk', unify_term alp c c', unify_opt_term alp t t')
       | GLocalPattern ((p,ids),id,bk,t), GLocalPattern ((p',_),_,bk',t') ->
          let alp, p = unify_pat alp p p' in
-         alp, CAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
+         alp, DAst.make ?loc @@ GLocalPattern ((p,ids), id, unify_binding_kind bk bk', unify_term alp t t')
       | _ -> raise No_match in
     let rec unify alp bl bl' =
     match bl, bl' with
@@ -819,19 +839,22 @@ let bind_bindinglist_as_term_env alp (terms,onlybinders,termlists,binderlists) v
     let unify_pat p p' =
       if cases_pattern_eq (map_cases_pattern_name_left (name_app (rename_var (snd alp))) p) p' then p'
       else raise No_match in
-    let unify_term_binder c = CAst.(map (fun b' ->
-      match c, b' with
-      | { v = GVar id}, GLocalAssum (na', bk', t') ->
+    let unify_term_binder c = DAst.(map (fun b' ->
+      match DAst.get c, b' with
+      | GVar id, GLocalAssum (na', bk', t') ->
          GLocalAssum (unify_id id na', bk', t')
-      | c, GLocalPattern ((p',ids), id, bk', t') ->
+      | _, GLocalPattern ((p',ids), id, bk', t') ->
          let p = pat_binder_of_term c in
          GLocalPattern ((unify_pat p p',ids), id, bk', t')
       | _ -> raise No_match )) in
     let rec unify cl bl' =
     match cl, bl' with
     | [], [] -> []
-    | c :: cl, { CAst.v = GLocalDef ( _, _, _, t) } :: bl' -> unify cl bl'
-    | c :: cl, b' :: bl' -> unify_term_binder c b' :: unify cl bl'
+    | c :: cl, b' :: bl' ->
+      begin match DAst.get b' with
+      | GLocalDef ( _, _, _, t) -> unify cl bl'
+      | _ -> unify_term_binder c b' :: unify cl bl'
+      end
     | _ -> raise No_match in
     let bl = unify cl bl' in
     let sigma = (terms,onlybinders,termlists,Id.List.remove_assoc var binderlists) in
@@ -872,7 +895,7 @@ let match_names metas (alp,sigma) na1 na2 = match (na1,na2) with
   | _ -> raise No_match
 
 let rec match_cases_pattern_binders metas acc pat1 pat2 =
-  match CAst.(pat1.v, pat2.v) with
+  match DAst.get pat1, DAst.get pat2 with
   | PatVar na1, PatVar na2 -> match_names metas acc na1 na2
   | PatCstr (c1,patl1,na1), PatCstr (c2,patl2,na2)
       when eq_constructor c1 c2 && Int.equal (List.length patl1) (List.length patl2) ->
@@ -882,21 +905,29 @@ let rec match_cases_pattern_binders metas acc pat1 pat2 =
 
 let glue_letin_with_decls = true
 
-let rec match_iterated_binders islambda decls bi = CAst.(with_loc_val (fun ?loc -> function
-  | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))])})
-      when islambda && Id.equal p e ->
-      match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
-  | GLambda (na,bk,t,b) when islambda ->
-      match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
-  | GProd (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b))]) } )
-      when not islambda && Id.equal p e ->
-      match_iterated_binders islambda ((CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
-  | GProd ((Name _ as na),bk,t,b) when not islambda ->
-      match_iterated_binders islambda ((CAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+let rec match_iterated_binders islambda decls bi = DAst.(with_loc_val (fun ?loc -> function
+  | GLambda (na,bk,t,b) as b0 ->
+    begin match na, DAst.get b with
+    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
+      when islambda && is_gvar p e ->
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+    | _, _ when islambda ->
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+    | _ -> (decls, DAst.make ?loc b0)
+    end
+  | GProd (na,bk,t,b) as b0 ->
+    begin match na, DAst.get b with
+    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b))])
+      when not islambda && is_gvar p e ->
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t))::decls) b
+    | Name _, _ when not islambda ->
+      match_iterated_binders islambda ((DAst.make ?loc @@ GLocalAssum(na,bk,t))::decls) b
+    | _ -> (decls, DAst.make ?loc b0)
+    end
   | GLetIn (na,c,t,b) when glue_letin_with_decls ->
       match_iterated_binders islambda
-	((CAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
-  | b -> (decls, CAst.make ?loc b)
+	((DAst.make ?loc @@ GLocalDef (na,Explicit (*?*), c,t))::decls) b
+  | b -> (decls, DAst.make ?loc b)
   )) bi
 
 let remove_sigma x (terms,onlybinders,termlists,binderlists) =
@@ -948,7 +979,7 @@ let match_termlist match_fun alp metas sigma rest x y iter termin lassoc =
   else
     bind_termlist_env alp sigma x l
 
-let does_not_come_from_already_eta_expanded_var =
+let does_not_come_from_already_eta_expanded_var glob =
   (* This is hack to avoid looping on a rule with rhs of the form *)
   (* "?f (fun ?x => ?g)" since otherwise, matching "F H" expands in *)
   (* "F (fun x => H x)" and "H x" is recursively matched against the same *)
@@ -958,12 +989,14 @@ let does_not_come_from_already_eta_expanded_var =
   (* The following test is then an approximation of what can be done *)
   (* optimally (whether other looping situations can occur remains to be *)
   (* checked). *)
-  function { CAst.v = GVar _ } -> false | _ -> true
+  match DAst.get glob with GVar _ -> false | _ -> true
+
+let is_var c = match DAst.get c with GVar _ -> true | _ -> false
 
 let rec match_ inner u alp metas sigma a1 a2 =
   let open CAst in
   let loc = a1.loc in
-  match a1.v, a2 with
+  match DAst.get a1, a2 with
   (* Matching notation variable *)
   | r1, NVar id2 when is_term_meta id2 metas -> bind_term_env alp sigma id2 a1
   | GVar id1, NVar id2 when is_onlybinding_meta id2 metas -> bind_binding_as_term_env alp sigma id2 id1
@@ -973,50 +1006,62 @@ let rec match_ inner u alp metas sigma a1 a2 =
   | r1, NList (x,y,iter,termin,lassoc) ->
       match_termlist (match_hd u alp) alp metas sigma a1 x y iter termin lassoc
 
-  (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
-  | GLambda (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e},_)],[(_,(ids,[cp],b1))])}),
-    NBinderList (x,_,NLambda (Name _id2,_,b2),termin) when Id.equal p e ->
-      let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
+  | GLambda (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
+    begin match na1, DAst.get b1, iter with
+    (* "λ p, let 'cp = p in t" -> "λ 'cp, t" *)
+    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), NLambda (Name _, _, _) when is_gvar p e ->
+      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern((cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
-
-  (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
-  | GLambda (na1,bk,t1,b1), NBinderList (x,_,NLambda (Name _id2,_,b2),termin)->
-      let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
+    (* Matching recursive notations for binders: ad hoc cases supporting let-in *)
+    | _, _, NLambda (Name _,_,_) ->
+      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Lambda itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
+    (* Matching recursive notations for binders: general case *)
+    | _, _, _ ->
+      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+    end
 
-  (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
-  | GProd (Name p,bk,t1, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))]) } ),
-    NBinderList (x,_,NProd (Name _id2,_,b2),(NVar v as termin)) when Id.equal p e ->
-      let (decls,b) = match_iterated_binders true [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
+  | GProd (na1, bk, t1, b1), NBinderList (x,y,iter,termin) ->
+    (* "∀ p, let 'cp = p in t" -> "∀ 'cp, t" *)
+    begin match na1, DAst.get b1, iter, termin with
+    | Name p, GCases (LetPatternStyle,None,[(e, _)],[(_,(ids,[cp],b1))]), NProd (Name _,_,_), NVar _ when is_gvar p e ->
+      let (decls,b) = match_iterated_binders true [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] b1 in
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
-
-  | GProd (na1,bk,t1,b1), NBinderList (x,_,NProd (Name _id2,_,b2),termin)
-      when na1 != Anonymous ->
-      let (decls,b) = match_iterated_binders false [CAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
+    | _, _,  NProd (Name _,_,_), _ when na1 != Anonymous ->
+      let (decls,b) = match_iterated_binders false [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] b1 in
       (* TODO: address the possibility that termin is a Prod itself *)
       let alp,sigma = bind_bindinglist_env alp sigma x decls in
       match_in u alp metas sigma b termin
+    (* Matching recursive notations for binders: general case *)
+    | _, _, _, _ ->
+      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+    end
+
   (* Matching recursive notations for binders: general case *)
   | _r, NBinderList (x,y,iter,termin) ->
-      match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
+       match_binderlist_with_app (match_hd u) alp metas sigma a1 x y iter termin
 
   (* Matching individual binders as part of a recursive pattern *)
-  | GLambda (Name p,bk,t, { v = GCases (LetPatternStyle,None,[({ v = GVar e },_)],[(_,(ids,[cp],b1))])}),
-    NLambda (Name id,_,b2)
-      when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t)] in
+  | GLambda (na1, bk, t1, b1), NLambda (na2, t2, b2) ->
+    begin match na1, DAst.get b1, na2 with
+    | Name p, GCases (LetPatternStyle,None,[(e,_)],[(_,(ids,[cp],b1))]), Name id
+      when is_var e && is_bindinglist_meta id metas ->
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((cp,ids),p,bk,t1)] in
       match_in u alp metas sigma b1 b2
-  | GLambda (na,bk,t,b1), NLambda (Name id,_,b2)
-      when is_bindinglist_meta id metas ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in
+    | _, _, Name id when is_bindinglist_meta id metas ->
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na1,bk,t1)] in
       match_in u alp metas sigma b1 b2
+    | _ ->
+      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
+    end
+
   | GProd (na,bk,t,b1), NProd (Name id,_,b2)
       when is_bindinglist_meta id metas && na != Anonymous ->
-      let alp,sigma = bind_bindinglist_env alp sigma id [CAst.make ?loc @@ GLocalAssum (na,bk,t)] in
+      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalAssum (na,bk,t)] in
       match_in u alp metas sigma b1 b2
 
   (* Matching compositionally *)
@@ -1028,13 +1073,11 @@ let rec match_ inner u alp metas sigma a1 a2 =
 	if n1 < n2 then
 	  let l21,l22 = List.chop (n2-n1) l2 in f1,l1, NApp (f2,l21), l22
 	else if n1 > n2 then
-	  let l11,l12 = List.chop (n1-n2) l1 in CAst.make ?loc @@ GApp (f1,l11),l12, f2,l2
+	  let l11,l12 = List.chop (n1-n2) l1 in DAst.make ?loc @@ GApp (f1,l11),l12, f2,l2
 	else f1,l1, f2, l2 in
       let may_use_eta = does_not_come_from_already_eta_expanded_var f1 in
       List.fold_left2 (match_ may_use_eta u alp metas)
         (match_in u alp metas sigma f1 f2) l1 l2
-  | GLambda (na1,_,t1,b1), NLambda (na2,t2,b2) ->
-     match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
   | GProd (na1,_,t1,b1), NProd (na2,t2,b2) ->
      match_binders u alp metas na1 na2 (match_in u alp metas sigma t1 t2) b1 b2
   | GLetIn (na1,b1,_,c1), NLetIn (na2,b2,None,c2)
@@ -1101,17 +1144,17 @@ let rec match_ inner u alp metas sigma a1 a2 =
       let avoid =
         free_glob_vars a1 @ (* as in Namegen: *) glob_visible_short_qualid a1 in
       let id' = Namegen.next_ident_away id avoid in
-      let t1 = CAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
+      let t1 = DAst.make @@ GHole(Evar_kinds.BinderType (Name id'),Misctypes.IntroAnonymous,None) in
       let sigma = match t2 with
       | NHole _ -> sigma
       | NVar id2 -> bind_term_env alp sigma id2 t1
       | _ -> assert false in
       let (alp,sigma) =
         if is_bindinglist_meta id metas then
-          bind_bindinglist_env alp sigma id [CAst.make @@ GLocalAssum (Name id',Explicit,t1)]
+          bind_bindinglist_env alp sigma id [DAst.make @@ GLocalAssum (Name id',Explicit,t1)]
         else
           match_names metas (alp,sigma) (Name id') na in
-      match_in u alp metas sigma (mkGApp a1 (CAst.make @@ GVar id')) b2
+      match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2
 
   | (GRec _ | GEvar _), _
   | _,_ -> raise No_match
@@ -1132,7 +1175,7 @@ and match_equations u alp metas sigma (_,(_,patl1,rhs1)) (patl2,rhs2) =
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-let term_of_binder bi = CAst.make @@ match bi with
+let term_of_binder bi = DAst.make @@ match bi with
   | Name id -> GVar id
   | Anonymous -> GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None)
 
@@ -1145,7 +1188,7 @@ let match_notation_constr u c (metas,pat) =
     with Not_found ->
       (* Happens for binders bound to Anonymous *)
       (* Find a better way to propagate Anonymous... *)
-      CAst.make @@GVar x in
+      DAst.make @@GVar x in
   List.fold_right (fun (x,(scl,typ)) (terms',termlists',binders') ->
     match typ with
     | NtnTypeConstr ->
@@ -1185,8 +1228,7 @@ let match_cases_pattern_list match_fun metas sigma rest x y iter termin lassoc =
   (terms,onlybinders,(x,if lassoc then l else List.rev l)::termlists, binderlists)
 
 let rec match_cases_pattern metas (terms,(),termlists,() as sigma) a1 a2 =
- let open CAst in
- match a1.v, a2 with
+ match DAst.get a1, a2 with
   | r1, NVar id2 when Id.List.mem_assoc id2 metas -> (bind_env_cases_pattern sigma id2 a1),(0,[])
   | PatVar Anonymous, NHole _ -> sigma,(0,[])
   | PatCstr ((ind,_ as r1),largs,_), NRef (ConstructRef r2) when eq_constructor r1 r2 ->