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.

8 files changed, 244 insertions, 197 deletions

diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 63775d737..7455587c0 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -94,7 +94,7 @@ let msg_may_need_inversion () =
 
 (* Utils *)
 let make_anonymous_patvars n =
-  List.make n (CAst.make @@ PatVar Anonymous)
+  List.make n (DAst.make @@ PatVar Anonymous)
 
 (* We have x1:t1...xn:tn,xi':ti,y1..yk |- c and re-generalize
    over xi:ti to get x1:t1...xn:tn,xi':ti,y1..yk |- c[xi:=xi'] *)
@@ -177,7 +177,7 @@ and build_glob_pattern args = function
   | Top -> args
   | MakeConstructor (pci, rh) ->
       glob_pattern_of_partial_history
-	[CAst.make @@ PatCstr (pci, args, Anonymous)] rh
+	[DAst.make @@ PatCstr (pci, args, Anonymous)] rh
 
 let complete_history = glob_pattern_of_partial_history []
 
@@ -187,12 +187,12 @@ let pop_history_pattern = function
   | Continuation (0, l, Top) ->
       Result (List.rev l)
   | Continuation (0, l, MakeConstructor (pci, rh)) ->
-      feed_history (CAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
+      feed_history (DAst.make @@ PatCstr (pci,List.rev l,Anonymous)) rh
   | _ ->
       anomaly (Pp.str "Constructor not yet filled with its arguments.")
 
 let pop_history h =
-  feed_history (CAst.make @@ PatVar Anonymous) h
+  feed_history (DAst.make @@ PatVar Anonymous) h
 
 (* Builds a continuation expecting [n] arguments and building [ci] applied
    to this [n] arguments *)
@@ -273,8 +273,10 @@ type 'a pattern_matching_problem =
 
 let rec find_row_ind = function
     [] -> None
-  | { CAst.v = PatVar _ } :: l -> find_row_ind l
-  | { CAst.v = PatCstr(c,_,_) ; loc } :: _ -> Some (loc,c)
+  | p :: l ->
+    match DAst.get p with
+    | PatVar _ -> find_row_ind l
+    | PatCstr(c,_,_) -> Some (p.CAst.loc,c)
 
 let inductive_template evdref env tmloc ind =
   let indu = evd_comb1 (Evd.fresh_inductive_instance env) evdref ind in
@@ -348,7 +350,7 @@ let find_tomatch_tycon evdref env loc = function
       empty_tycon,None
 
 let make_return_predicate_ltac_lvar sigma na tm c lvar =
-  match na, tm.CAst.v with
+  match na, DAst.get tm with
   | Name id, (GVar id' | GRef (Globnames.VarRef id', _)) when Id.equal id id' ->
      if Id.Map.mem id lvar.ltac_genargs then
        let ltac_genargs = Id.Map.remove id lvar.ltac_genargs in
@@ -447,7 +449,7 @@ let current_pattern eqn =
     | pat::_ -> pat
     | [] -> anomaly (Pp.str "Empty list of patterns.")
 
-let alias_of_pat = CAst.with_val (function
+let alias_of_pat = DAst.with_val (function
   | PatVar name -> name
   | PatCstr(_,_,name) -> name
   )
@@ -493,13 +495,14 @@ let rec adjust_local_defs ?loc = function
   | (pat :: pats, LocalAssum _ :: decls) ->
       pat :: adjust_local_defs ?loc (pats,decls)
   | (pats, LocalDef _ :: decls) ->
-      (CAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls)
+      (DAst.make ?loc @@ PatVar Anonymous) :: adjust_local_defs ?loc (pats,decls)
   | [], [] -> []
   | _ -> raise NotAdjustable
 
-let check_and_adjust_constructor env ind cstrs = function
-  | { CAst.v = PatVar _ } as pat -> pat
-  | { CAst.v = PatCstr (((_,i) as cstr),args,alias) ; loc } as pat ->
+let check_and_adjust_constructor env ind cstrs pat = match DAst.get pat with
+  | PatVar _ -> pat
+  | PatCstr (((_,i) as cstr),args,alias) ->
+      let loc = pat.CAst.loc in
       (* Check it is constructor of the right type *)
       let ind' = inductive_of_constructor cstr in
       if eq_ind ind' ind then
@@ -510,7 +513,7 @@ let check_and_adjust_constructor env ind cstrs = function
 	else
 	  try
 	    let args' = adjust_local_defs ?loc (args, List.rev ci.cs_args)
-	    in CAst.make ?loc @@ PatCstr (cstr, args', alias)
+	    in DAst.make ?loc @@ PatCstr (cstr, args', alias)
 	  with NotAdjustable ->
 	    error_wrong_numarg_constructor ?loc env cstr nb_args_constr
       else
@@ -522,9 +525,12 @@ let check_and_adjust_constructor env ind cstrs = function
 
 let check_all_variables env sigma typ mat =
   List.iter
-    (fun eqn -> match current_pattern eqn with
-       | { CAst.v = PatVar id } -> ()
-       | { CAst.v = PatCstr (cstr_sp,_,_); loc } ->
+    (fun eqn ->
+      let pat = current_pattern eqn in
+      match DAst.get pat with
+       | PatVar id -> ()
+       | PatCstr (cstr_sp,_,_) ->
+          let loc = pat.CAst.loc in
 	   error_bad_pattern ?loc env sigma cstr_sp typ)
     mat
 
@@ -549,9 +555,9 @@ let occur_in_rhs na rhs =
     | Anonymous -> false
     | Name id -> Id.List.mem id rhs.rhs_vars
 
-let is_dep_patt_in eqn = function
-  | { CAst.v = PatVar name } -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
-  | { CAst.v = PatCstr _ } -> true
+let is_dep_patt_in eqn pat = match DAst.get pat with
+  | PatVar name -> Flags.is_program_mode () || occur_in_rhs name eqn.rhs
+  | PatCstr _ -> true
 
 let mk_dep_patt_row (pats,_,eqn) =
   List.map (is_dep_patt_in eqn) pats
@@ -771,7 +777,7 @@ let recover_and_adjust_alias_names names sign =
   | x::names, LocalAssum (_,t)::sign ->
       (x, LocalAssum (alias_of_pat x,t)) :: aux (names,sign)
   | names, (LocalDef (na,_,_) as decl)::sign ->
-      (CAst.make @@ PatVar na, decl) :: aux (names,sign)
+      (DAst.make @@ PatVar na, decl) :: aux (names,sign)
   | _ -> assert false
   in
   List.split (aux (names,sign))
@@ -987,7 +993,7 @@ let use_unit_judge evd =
     evd', j
 
 let add_assert_false_case pb tomatch =
-  let pats = List.map (fun _ -> CAst.make @@ PatVar Anonymous) tomatch in
+  let pats = List.map (fun _ -> DAst.make @@ PatVar Anonymous) tomatch in
   let aliasnames =
     List.map_filter (function Alias _ | NonDepAlias -> Some Anonymous | _ -> None) tomatch
   in
@@ -1184,9 +1190,9 @@ let postprocess_dependencies evd tocheck brs tomatch pred deps cs =
 (************************************************************************)
 (* Sorting equations by constructor *)
 
-let rec irrefutable env = function
-  | { CAst.v = PatVar name } -> true
-  | { CAst.v = PatCstr (cstr,args,_) } ->
+let rec irrefutable env pat = match DAst.get pat with
+  | PatVar name -> true
+  | PatCstr (cstr,args,_) ->
       let ind = inductive_of_constructor cstr in
       let (_,mip) = Inductive.lookup_mind_specif env ind in
       let one_constr = Int.equal (Array.length mip.mind_user_lc) 1 in
@@ -1206,15 +1212,15 @@ let group_equations pb ind current cstrs mat =
       (fun eqn () ->
 	 let rest = remove_current_pattern eqn in
 	 let pat = current_pattern eqn in
-	 match check_and_adjust_constructor pb.env ind cstrs pat with
-	   | { CAst.v = PatVar name } ->
+	 match DAst.get (check_and_adjust_constructor pb.env ind cstrs pat) with
+	   | PatVar name ->
 	       (* This is a default clause that we expand *)
 	       for i=1 to Array.length cstrs do
 		 let args = make_anonymous_patvars cstrs.(i-1).cs_nargs in
 		 brs.(i-1) <- (args, name, rest) :: brs.(i-1)
 	       done;
 	       if !only_default == None then only_default := Some true
-	   | { CAst.v = PatCstr (((_,i)),args,name) ; loc } ->
+	   | PatCstr (((_,i)),args,name) ->
 	       (* This is a regular clause *)
 	       only_default := Some false;
 	       brs.(i-1) <- (args, name, rest) :: brs.(i-1)) mat () in
@@ -1745,16 +1751,16 @@ let build_tycon ?loc env tycon_env s subst tycon extenv evdref t =
 let build_inversion_problem loc env sigma tms t =
   let make_patvar t (subst,avoid) =
     let id = next_name_away (named_hd env sigma t Anonymous) avoid in
-    CAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
+    DAst.make @@ PatVar (Name id), ((id,t)::subst, id::avoid) in
   let rec reveal_pattern t (subst,avoid as acc) =
     match EConstr.kind sigma (whd_all env sigma t) with
-    | Construct (cstr,u) -> CAst.make (PatCstr (cstr,[],Anonymous)), acc
+    | Construct (cstr,u) -> DAst.make (PatCstr (cstr,[],Anonymous)), acc
     | App (f,v) when isConstruct sigma f ->
 	let cstr,u = destConstruct sigma f in
 	let n = constructor_nrealargs_env env cstr in
 	let l = List.lastn n (Array.to_list v) in
 	let l,acc = List.fold_right_map reveal_pattern l acc in
-	CAst.make (PatCstr (cstr,l,Anonymous)), acc
+	DAst.make (PatCstr (cstr,l,Anonymous)), acc
     | _ -> make_patvar t acc in
   let rec aux n env acc_sign tms acc =
     match tms with
@@ -1830,7 +1836,7 @@ let build_inversion_problem loc env sigma tms t =
       (* No need for a catch all clause *)
       []
     else
-      [ { patterns = List.map (fun _ -> CAst.make @@ PatVar Anonymous) patl;
+      [ { patterns = List.map (fun _ -> DAst.make @@ PatVar Anonymous) patl;
           alias_stack = [];
           eqn_loc = None;
           used = ref false;
@@ -2094,14 +2100,14 @@ let mk_JMeq evdref typ x typ' y =
 let mk_JMeq_refl evdref typ x = 
   papp evdref coq_JMeq_refl [| typ; x |]
 
-let hole na = CAst.make @@
+let hole na = DAst.make @@
   GHole (Evar_kinds.QuestionMark (Evar_kinds.Define false,na),
          Misctypes.IntroAnonymous, None)
 
 let constr_of_pat env evdref arsign pat avoid =
   let rec typ env (ty, realargs) pat avoid =
     let loc = pat.CAst.loc in
-    match pat.CAst.v with
+    match DAst.get pat with
     | PatVar name ->
 	let name, avoid = match name with
 	    Name n -> name, avoid
@@ -2109,7 +2115,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	      let previd, id = prime avoid (Name (Id.of_string "wildcard")) in
 		Name id, id :: avoid
 	in
-	  ((CAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
+	  ((DAst.make ?loc @@ PatVar name), [LocalAssum (name, ty)] @ realargs, mkRel 1, ty,
 	   (List.map (fun x -> mkRel 1) realargs), 1, avoid)
     | PatCstr (((_, i) as cstr),args,alias) ->
 	let cind = inductive_of_constructor cstr in
@@ -2140,7 +2146,7 @@ let constr_of_pat env evdref arsign pat avoid =
 	in
 	let args = List.rev args in
 	let patargs = List.rev patargs in
-	let pat' = CAst.make ?loc @@ PatCstr (cstr, patargs, alias) in
+	let pat' = DAst.make ?loc @@ PatCstr (cstr, patargs, alias) in
 	let cstr = mkConstructU (on_snd EInstance.make ci.cs_cstr) in
 	let app = applist (cstr, List.map (lift (List.length sign)) params) in
 	let app = applist (app, args) in
@@ -2196,18 +2202,18 @@ let vars_of_ctx sigma ctx =
       match decl with
 	| LocalDef (na,t',t) when is_topvar sigma t' ->
 	    prev,
-	    (CAst.make @@ GApp (
-		(CAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
-		   [hole na; CAst.make @@ GVar prev])) :: vars
+	    (DAst.make @@ GApp (
+		(DAst.make @@ GRef (delayed_force coq_eq_refl_ref, None)), 
+		   [hole na; DAst.make @@ GVar prev])) :: vars
 	| _ ->
 	    match RelDecl.get_name decl with
 		Anonymous -> invalid_arg "vars_of_ctx"
-	      | Name n -> n, (CAst.make @@ GVar n) :: vars)
+	      | Name n -> n, (DAst.make @@ GVar n) :: vars)
       ctx (Id.of_string "vars_of_ctx_error", [])
   in List.rev y
 
 let rec is_included x y =
-  match CAst.(x.v, y.v) with
+  match DAst.get x, DAst.get y with
     | PatVar _, _ -> true
     | _, PatVar _ -> true
     | PatCstr ((_, i), args, alias), PatCstr ((_, i'), args', alias')  ->
@@ -2325,13 +2331,13 @@ let constrs_of_pats typing_fun env evdref eqns tomatchs sign neqs arity =
 	 let branch_name = Id.of_string ("program_branch_" ^ (string_of_int !i)) in
 	 let branch_decl = LocalDef (Name branch_name, lift !i bbody, lift !i btype) in
 	 let branch =
-	   let bref = CAst.make @@ GVar branch_name in
+	   let bref = DAst.make @@ GVar branch_name in
 	     match vars_of_ctx !evdref rhs_rels with
 		 [] -> bref
-	       | l  -> CAst.make @@ GApp (bref, l)
+	       | l  -> DAst.make @@ GApp (bref, l)
 	 in
 	 let branch = match ineqs with
-	     Some _ -> CAst.make @@ GApp (branch, [ hole Anonymous ])
+	     Some _ -> DAst.make @@ GApp (branch, [ hole Anonymous ])
 	   | None -> branch
 	 in
 	 incr i;
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 535a62046..fc0a650bc 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -77,8 +77,8 @@ let apply_pattern_coercion ?loc pat p =
   List.fold_left
     (fun pat (co,n) ->
        let f i =
-         if i<n then (CAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in
-        CAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
+         if i<n then (DAst.make ?loc @@ Glob_term.PatVar Anonymous) else pat in
+        DAst.make ?loc @@ Glob_term.PatCstr (co, List.init (n+1) f, Anonymous))
     pat p
 
 (* raise Not_found if no coercion found *)
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index b9cb7ba1b..1eb22cdb8 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -28,6 +28,10 @@ open Misctypes
 open Decl_kinds
 open Context.Named.Declaration
 
+type _ delay =
+| Now : 'a delay
+| Later : [ `thunk ] delay
+
 (** Should we keep details of universes during detyping ? *)
 let print_universes = Flags.univ_print
 
@@ -277,7 +281,7 @@ let rec decomp_branch tags nal b (avoid,env as e) sigma c =
       (avoid', add_name_opt na' body t env) sigma c
 
 let rec build_tree na isgoal e sigma ci cl =
-  let mkpat n rhs pl = CAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
+  let mkpat n rhs pl = DAst.make @@ PatCstr((ci.ci_ind,n+1),pl,update_name sigma na rhs) in
   let cnl = ci.ci_pp_info.cstr_tags in
   let cna = ci.ci_cstr_nargs in
   List.flatten
@@ -300,7 +304,7 @@ and align_tree nal isgoal (e,c as rhs) sigma = match nal with
 	      List.map (fun (hd,rest) -> pat::hd,rest) lines)
 	    clauses)
     | _ ->
-	let pat = CAst.make @@ PatVar(update_name sigma na rhs) in
+	let pat = DAst.make @@ PatVar(update_name sigma na rhs) in
 	let mat = align_tree nal isgoal rhs sigma in
 	List.map (fun (hd,rest) -> pat::hd,rest) mat
 
@@ -323,7 +327,7 @@ let is_nondep_branch sigma c l =
 
 let extract_nondep_branches test c b l =
   let rec strip l r =
-    match r.CAst.v, l with
+    match DAst.get r, l with
       | r', [] -> r
       | GLambda (_,_,_,t), false::l -> strip l t
       | GLetIn (_,_,_,t), true::l -> strip l t
@@ -333,7 +337,7 @@ let extract_nondep_branches test c b l =
 
 let it_destRLambda_or_LetIn_names l c =
   let rec aux l nal c =
-    match c.CAst.v, l with
+    match DAst.get c, l with
       | _, [] -> (List.rev nal,c)
       | GLambda (na,_,_,c), false::l -> aux l (na::nal) c
       | GLetIn (na,_,_,c), true::l -> aux l (na::nal) c
@@ -347,11 +351,11 @@ let it_destRLambda_or_LetIn_names l c =
 	    x
 	  in
 	  let x = next (free_glob_vars c) in
-	  let a = CAst.make @@ GVar x in
+	  let a = DAst.make @@ GVar x in
 	  aux l (Name x :: nal)
-            (match c with
-              | { loc; CAst.v = GApp (p,l) } -> CAst.make ?loc @@ GApp (p,l@[a])
-              | _ -> CAst.make @@ GApp (c,[a]))
+            (match DAst.get c with
+              | GApp (p,l) -> DAst.make ?loc:c.CAst.loc @@ GApp (p,l@[a])
+              | _ -> DAst.make @@ GApp (c,[a]))
   in aux l [] c
 
 let detype_case computable detype detype_eqns testdep avoid data p c bl =
@@ -367,7 +371,7 @@ let detype_case computable detype detype_eqns testdep avoid data p c bl =
         | None -> Anonymous, None, None
         | Some p ->
             let nl,typ = it_destRLambda_or_LetIn_names k p in
-	    let n,typ = match typ.CAst.v with
+	    let n,typ = match DAst.get typ with
               | GLambda (x,_,t,c) -> x, c
 	      | _ -> Anonymous, typ in
 	    let aliastyp =
@@ -437,12 +441,20 @@ let detype_instance sigma l =
   if Univ.Instance.is_empty l then None
   else Some (List.map (detype_level sigma) (Array.to_list (Univ.Instance.to_array l)))
 
-let rec detype flags avoid env sigma t = CAst.make @@
+let delay (type a) (d : a delay) (f : a delay -> _ -> _ -> _ -> _ -> _ -> a glob_constr_r) flags env avoid sigma t : a glob_constr_g =
+  match d with
+  | Now -> DAst.make (f d flags env avoid sigma t)
+  | Later -> DAst.delay (fun () -> f d flags env avoid sigma t)
+
+let rec detype d flags avoid env sigma t =
+  delay d detype_r flags avoid env sigma t
+
+and detype_r d flags avoid env sigma t =
   match EConstr.kind sigma (collapse_appl sigma t) with
     | Rel n ->
       (try match lookup_name_of_rel n (fst env) with
 	 | Name id   -> GVar id
-	 | Anonymous -> (!detype_anonymous n).CAst.v
+	 | Anonymous -> GVar (!detype_anonymous n)
        with Not_found ->
 	 let s = "_UNBOUND_REL_"^(string_of_int n)
 	 in GVar (Id.of_string s))
@@ -455,44 +467,44 @@ let rec detype flags avoid env sigma t = CAst.make @@
 	 with Not_found -> GVar id)
     | Sort s -> GSort (detype_sort sigma (ESorts.kind sigma s))
     | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
-        (detype flags avoid env sigma c1).CAst.v
+        DAst.get (detype d flags avoid env sigma c1)
     | Cast (c1,k,c2) ->
-        let d1 = detype flags avoid env sigma c1 in
-	let d2 = detype flags avoid env sigma c2 in
+        let d1 = detype d flags avoid env sigma c1 in
+	let d2 = detype d flags avoid env sigma c2 in
     let cast = match k with
     | VMcast -> CastVM d2
     | NATIVEcast -> CastNative d2
     | _ -> CastConv d2
     in
 	GCast(d1,cast)
-    | Prod (na,ty,c) -> detype_binder flags BProd avoid env sigma na None ty c
-    | Lambda (na,ty,c) -> detype_binder flags BLambda avoid env sigma na None ty c
-    | LetIn (na,b,ty,c) -> detype_binder flags BLetIn avoid env sigma na (Some b) ty c
+    | Prod (na,ty,c) -> detype_binder d flags BProd avoid env sigma na None ty c
+    | Lambda (na,ty,c) -> detype_binder d flags BLambda avoid env sigma na None ty c
+    | LetIn (na,b,ty,c) -> detype_binder d flags BLetIn avoid env sigma na (Some b) ty c
     | App (f,args) ->
       let mkapp f' args' = 
- 	match f'.CAst.v with
+ 	match DAst.get f' with
  	| GApp (f',args'') -> 
  	  GApp (f',args''@args')
  	| _ -> GApp (f',args')
       in
-      mkapp (detype flags avoid env sigma f)
-        (Array.map_to_list (detype flags avoid env sigma) args)
+      mkapp (detype d flags avoid env sigma f)
+        (Array.map_to_list (detype d flags avoid env sigma) args)
     | Const (sp,u) -> GRef (ConstRef sp, detype_instance sigma u)
     | Proj (p,c) ->
       let noparams () = 
 	let pb = Environ.lookup_projection p (snd env) in
 	let pars = pb.Declarations.proj_npars in
-	let hole = CAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
+	let hole = DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None) in
 	let args = List.make pars hole in
- 	  GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None),
-		(args @ [detype flags avoid env sigma c]))
+ 	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None),
+		(args @ [detype d flags avoid env sigma c]))
       in
       if fst flags || !Flags.in_debugger || !Flags.in_toplevel then
 	try noparams ()
 	with _ ->
 	    (* lax mode, used by debug printers only *) 
-	  GApp (CAst.make @@ GRef (ConstRef (Projection.constant p), None), 
-		[detype flags avoid env sigma c])
+	  GApp (DAst.make @@ GRef (ConstRef (Projection.constant p), None), 
+		[detype d flags avoid env sigma c])
       else 
 	if print_primproj_compatibility () && Projection.unfolded p then
 	  (** Print the compatibility match version *)
@@ -509,12 +521,12 @@ let rec detype flags avoid env sigma t = CAst.make @@
 		substl (c :: List.rev args) body'
 	    with Retyping.RetypeError _ | Not_found -> 
 	      anomaly (str"Cannot detype an unfolded primitive projection.")
-	  in (detype flags avoid env sigma c').CAst.v
+	  in DAst.get (detype d flags avoid env sigma c')
 	else
 	  if print_primproj_params () then
 	    try
 	      let c = Retyping.expand_projection (snd env) sigma p c [] in
-              (detype flags avoid env sigma c).CAst.v
+              DAst.get (detype d flags avoid env sigma c)
 	    with Retyping.RetypeError _ -> noparams ()
 	  else noparams ()
 
@@ -542,23 +554,23 @@ let rec detype flags avoid env sigma t = CAst.make @@
           (Array.map_to_list (fun c -> (Id.of_string "__",c)) cl)
       in
         GEvar (id,
-               List.map (on_snd (detype flags avoid env sigma)) l)
+               List.map (on_snd (detype d flags avoid env sigma)) l)
     | Ind (ind_sp,u) ->
 	GRef (IndRef ind_sp, detype_instance sigma u)
     | Construct (cstr_sp,u) ->
 	GRef (ConstructRef cstr_sp, detype_instance sigma u)
     | Case (ci,p,c,bl) ->
 	let comp = computable sigma p (List.length (ci.ci_pp_info.ind_tags)) in
-	detype_case comp (detype flags avoid env sigma)
-	  (detype_eqns flags avoid env sigma ci comp)
+	detype_case comp (detype d flags avoid env sigma)
+	  (detype_eqns d flags avoid env sigma ci comp)
 	  (is_nondep_branch sigma) avoid
 	  (ci.ci_ind,ci.ci_pp_info.style,
 	   ci.ci_pp_info.cstr_tags,ci.ci_pp_info.ind_tags)
 	  (Some p) c bl
-    | Fix (nvn,recdef) -> detype_fix flags avoid env sigma nvn recdef
-    | CoFix (n,recdef) -> detype_cofix flags avoid env sigma n recdef
+    | Fix (nvn,recdef) -> detype_fix d flags avoid env sigma nvn recdef
+    | CoFix (n,recdef) -> detype_cofix d flags avoid env sigma n recdef
 
-and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
+and detype_fix d flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
@@ -567,14 +579,14 @@ and detype_fix flags avoid env sigma (vn,_ as nvn) (names,tys,bodies) =
       (avoid, env, []) names tys in
   let n = Array.length tys in
   let v = Array.map3
-    (fun c t i -> share_names flags (i+1) [] def_avoid def_env sigma c (lift n t))
+    (fun c t i -> share_names d flags (i+1) [] def_avoid def_env sigma c (lift n t))
     bodies tys vn in
   GRec(GFix (Array.map (fun i -> Some i, GStructRec) (fst nvn), snd nvn),Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-and detype_cofix flags avoid env sigma n (names,tys,bodies) =
+and detype_cofix d flags avoid env sigma n (names,tys,bodies) =
   let def_avoid, def_env, lfi =
     Array.fold_left2
       (fun (avoid, env, l) na ty ->
@@ -583,14 +595,14 @@ and detype_cofix flags avoid env sigma n (names,tys,bodies) =
       (avoid, env, []) names tys in
   let ntys = Array.length tys in
   let v = Array.map2
-    (fun c t -> share_names flags 0 [] def_avoid def_env sigma c (lift ntys t))
+    (fun c t -> share_names d flags 0 [] def_avoid def_env sigma c (lift ntys t))
     bodies tys in
   GRec(GCoFix n,Array.of_list (List.rev lfi),
        Array.map (fun (bl,_,_) -> bl) v,
        Array.map (fun (_,_,ty) -> ty) v,
        Array.map (fun (_,bd,_) -> bd) v)
 
-and share_names flags n l avoid env sigma c t =
+and share_names d flags n l avoid env sigma c t =
   match EConstr.kind sigma c, EConstr.kind sigma t with
     (* factorize even when not necessary to have better presentation *)
     | Lambda (na,t,c), Prod (na',t',c') ->
@@ -598,59 +610,59 @@ and share_names flags n l avoid env sigma c t =
             Name _, _ -> na
           | _, Name _ -> na'
           | _ -> na in
-        let t' = detype flags avoid env sigma t in
+        let t' = detype d flags avoid env sigma t in
 	let id = next_name_away na avoid in
         let avoid = id::avoid and env = add_name (Name id) None t env in
-        share_names flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
+        share_names d flags (n-1) ((Name id,Explicit,None,t')::l) avoid env sigma c c'
     (* May occur for fix built interactively *)
     | LetIn (na,b,t',c), _ when n > 0 ->
-        let t'' = detype flags avoid env sigma t' in
-        let b' = detype flags avoid env sigma b in
+        let t'' = detype d flags avoid env sigma t' in
+        let b' = detype d flags avoid env sigma b in
 	let id = next_name_away na avoid in
         let avoid = id::avoid and env = add_name (Name id) (Some b) t' env in
-        share_names flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
+        share_names d flags n ((Name id,Explicit,Some b',t'')::l) avoid env sigma c (lift 1 t)
     (* Only if built with the f/n notation or w/o let-expansion in types *)
     | _, LetIn (_,b,_,t) when n > 0 ->
-	share_names flags n l avoid env sigma c (subst1 b t)
+	share_names d flags n l avoid env sigma c (subst1 b t)
     (* If it is an open proof: we cheat and eta-expand *)
     | _, Prod (na',t',c') when n > 0 ->
-        let t'' = detype flags avoid env sigma t' in
+        let t'' = detype d flags avoid env sigma t' in
 	let id = next_name_away na' avoid in
         let avoid = id::avoid and env = add_name (Name id) None t' env in
         let appc = mkApp (lift 1 c,[|mkRel 1|]) in
-        share_names flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
+        share_names d flags (n-1) ((Name id,Explicit,None,t'')::l) avoid env sigma appc c'
     (* If built with the f/n notation: we renounce to share names *)
     | _ ->
         if n>0 then Feedback.msg_debug (strbrk "Detyping.detype: cannot factorize fix enough");
-        let c = detype flags avoid env sigma c in
-        let t = detype flags avoid env sigma t in
+        let c = detype d flags avoid env sigma c in
+        let t = detype d flags avoid env sigma t in
         (List.rev l,c,t)
 
-and detype_eqns flags avoid env sigma ci computable constructs consnargsl bl =
+and detype_eqns d flags avoid env sigma ci computable constructs consnargsl bl =
   try
     if !Flags.raw_print || not (reverse_matching ()) then raise Exit;
     let mat = build_tree Anonymous (snd flags) (avoid,env) sigma ci bl in
-    List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype flags avoid env sigma c))
+    List.map (fun (pat,((avoid,env),c)) -> Loc.tag ([],[pat],detype d flags avoid env sigma c))
       mat
   with e when CErrors.noncritical e ->
     Array.to_list
-      (Array.map3 (detype_eqn flags avoid env sigma) constructs consnargsl bl)
+      (Array.map3 (detype_eqn d flags avoid env sigma) constructs consnargsl bl)
 
-and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
+and detype_eqn d (lax,isgoal as flags) avoid env sigma constr construct_nargs branch =
   let make_pat x avoid env b body ty ids =
     if force_wildcard () && noccurn sigma 1 b then
-      CAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids
+      DAst.make @@ PatVar Anonymous,avoid,(add_name Anonymous body ty env),ids
     else
       let flag = if isgoal then RenamingForGoal else RenamingForCasesPattern (fst env,b) in
       let na,avoid' = compute_displayed_name_in sigma flag avoid x b in
-      CAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na
+      DAst.make (PatVar na),avoid',(add_name na body ty env),add_vname ids na
   in
   let rec buildrec ids patlist avoid env l b =
     match EConstr.kind sigma b, l with
       | _, [] -> Loc.tag @@
         (Id.Set.elements ids,
-         [CAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)],
-         detype flags avoid env sigma b)
+         [DAst.make @@ PatCstr(constr, List.rev patlist,Anonymous)],
+         detype d flags avoid env sigma b)
       | Lambda (x,t,b), false::l ->
 	    let pat,new_avoid,new_env,new_ids = make_pat x avoid env b None t ids in
             buildrec new_ids (pat::patlist) new_avoid new_env l b
@@ -663,7 +675,7 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
 	    buildrec ids patlist avoid env l c
 
       | _, true::l ->
-	    let pat = CAst.make @@ PatVar Anonymous in
+	    let pat = DAst.make @@ PatVar Anonymous in
             buildrec ids (pat::patlist) avoid env l b
 
       | _, false::l ->
@@ -678,23 +690,23 @@ and detype_eqn (lax,isgoal as flags) avoid env sigma constr construct_nargs bran
   in
   buildrec Id.Set.empty [] avoid env construct_nargs branch
 
-and detype_binder (lax,isgoal as flags) bk avoid env sigma na body ty c =
+and detype_binder d (lax,isgoal as flags) bk avoid env sigma na body ty c =
   let flag = if isgoal then RenamingForGoal else RenamingElsewhereFor (fst env,c) in
   let na',avoid' = match bk with
   | BLetIn -> compute_displayed_let_name_in sigma flag avoid na c
   | _ -> compute_displayed_name_in sigma flag avoid na c in
-  let r =  detype flags avoid' (add_name na' body ty env) sigma c in
+  let r =  detype d flags avoid' (add_name na' body ty env) sigma c in
   match bk with
-  | BProd   -> GProd (na',Explicit,detype (lax,false) avoid env sigma ty, r)
-  | BLambda -> GLambda (na',Explicit,detype (lax,false) avoid env sigma ty, r)
+  | BProd   -> GProd (na',Explicit,detype d (lax,false) avoid env sigma ty, r)
+  | BLambda -> GLambda (na',Explicit,detype d (lax,false) avoid env sigma ty, r)
   | BLetIn ->
-      let c = detype (lax,false) avoid env sigma (Option.get body) in
+      let c = detype d (lax,false) avoid env sigma (Option.get body) in
       (* Heuristic: we display the type if in Prop *)
       let s = try Retyping.get_sort_family_of (snd env) sigma ty with _ when !Flags.in_debugger || !Flags.in_toplevel -> InType (* Can fail because of sigma missing in debugger *) in
-      let t = if s != InProp  && not !Flags.raw_print then None else Some (detype (lax,false) avoid env sigma ty) in
+      let t = if s != InProp  && not !Flags.raw_print then None else Some (detype d (lax,false) avoid env sigma ty) in
       GLetIn (na', c, t, r)
 
-let detype_rel_context ?(lax=false) where avoid env sigma sign =
+let detype_rel_context d ?(lax=false) where avoid env sigma sign =
   let where = Option.map (fun c -> EConstr.it_mkLambda_or_LetIn c sign) where in
   let rec aux avoid env = function
   | [] -> []
@@ -716,15 +728,18 @@ let detype_rel_context ?(lax=false) where avoid env sigma sign =
 	      | LocalAssum _ -> None
 	      | LocalDef (_,b,_) -> Some b
       in
-      let b' = Option.map (detype (lax,false) avoid env sigma) b in
-      let t' = detype (lax,false) avoid env sigma t in
+      let b' = Option.map (detype d (lax,false) avoid env sigma) b in
+      let t' = detype d (lax,false) avoid env sigma t in
       (na',Explicit,b',t') :: aux avoid' (add_name na' b t env) rest
   in aux avoid env (List.rev sign)
 
 let detype_names isgoal avoid nenv env sigma t = 
-  detype (false,isgoal) avoid (nenv,env) sigma t
-let detype ?(lax=false) isgoal avoid env sigma t =
-  detype (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
+  detype Now (false,isgoal) avoid (nenv,env) sigma t
+let detype d ?(lax=false) isgoal avoid env sigma t =
+  detype d (lax,isgoal) avoid (names_of_rel_context env, env) sigma t
+
+let detype_rel_context d ?lax where avoid env sigma sign =
+  detype_rel_context d ?lax where avoid env sigma sign
 
 let detype_closed_glob ?lax isgoal avoid env sigma t =
   let open Context.Rel.Declaration in
@@ -736,7 +751,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
     | Name id -> Name (convert_id cl id)
     | Anonymous -> Anonymous
   in
-  let rec detype_closed_glob cl cg : Glob_term.glob_constr = CAst.map (function
+  let rec detype_closed_glob cl cg : Glob_term.glob_constr = DAst.map (function
     | GVar id ->
         (* if [id] is bound to a name. *)
         begin try
@@ -750,11 +765,11 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
              [Printer.pr_constr_under_binders_env] does. *)
           let assums = List.map (fun id -> LocalAssum (Name id,(* dummy *) mkProp)) b in
           let env = push_rel_context assums env in
-          (detype ?lax isgoal avoid env sigma c).CAst.v
+          DAst.get (detype Now ?lax isgoal avoid env sigma c)
         (* if [id] is bound to a [closed_glob_constr]. *)
         with Not_found -> try
           let {closure;term} = Id.Map.find id cl.untyped in
-          (detype_closed_glob closure term).CAst.v
+          DAst.get (detype_closed_glob closure term)
         (* Otherwise [id] stands for itself *)
         with Not_found ->
          GVar id
@@ -781,7 +796,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
         in
         GCases(sty,po,tml,eqns)
     | c ->
-        (Glob_ops.map_glob_constr (detype_closed_glob cl) cg).CAst.v
+        DAst.get (Glob_ops.map_glob_constr (detype_closed_glob cl) cg)
     ) cg
   in
   detype_closed_glob t.closure t.term
@@ -789,7 +804,7 @@ let detype_closed_glob ?lax isgoal avoid env sigma t =
 (**********************************************************************)
 (* Module substitution: relies on detyping                            *)
 
-let rec subst_cases_pattern subst = CAst.map (function
+let rec subst_cases_pattern subst = DAst.map (function
   | PatVar _ as pat -> pat
   | PatCstr (((kn,i),j),cpl,n) as pat ->
       let kn' = subst_mind subst kn
@@ -800,11 +815,11 @@ let rec subst_cases_pattern subst = CAst.map (function
 
 let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
 
-let rec subst_glob_constr subst = CAst.map (function
+let rec subst_glob_constr subst = DAst.map (function
   | GRef (ref,u) as raw ->
       let ref',t = subst_global subst ref in
 	if ref' == ref then raw else
-         (detype false [] (Global.env()) Evd.empty (EConstr.of_constr t)).CAst.v
+         DAst.get (detype Now false [] (Global.env()) Evd.empty (EConstr.of_constr t))
 
   | GSort _
   | GVar _
@@ -905,8 +920,8 @@ let rec subst_glob_constr subst = CAst.map (function
 let simple_cases_matrix_of_branches ind brs =
   List.map (fun (i,n,b) ->
       let nal,c = it_destRLambda_or_LetIn_names n b in
-      let mkPatVar na = CAst.make @@ PatVar na in
-      let p = CAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
+      let mkPatVar na = DAst.make @@ PatVar na in
+      let p = DAst.make @@ PatCstr ((ind,i+1),List.map mkPatVar nal,Anonymous) in
       let ids = List.map_filter Nameops.Name.to_option nal in
       Loc.tag @@ (ids,[p],c))
     brs
diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index 59f3f967d..67c852af3 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -16,6 +16,10 @@ open Mod_subst
 open Misctypes
 open Evd
 
+type _ delay =
+| Now : 'a delay
+| Later : [ `thunk ] delay
+
 (** Should we keep details of universes during detyping ? *)
 val print_universes : bool ref
 
@@ -33,12 +37,12 @@ val subst_glob_constr : substitution -> glob_constr -> glob_constr
 
 val detype_names : bool -> Id.t list -> names_context -> env -> evar_map -> constr -> glob_constr
 
-val detype : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> glob_constr
+val detype : 'a delay -> ?lax:bool -> bool -> Id.t list -> env -> evar_map -> constr -> 'a glob_constr_g
 
 val detype_sort : evar_map -> sorts -> glob_sort
 
-val detype_rel_context : ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
-  evar_map -> rel_context -> glob_decl list
+val detype_rel_context : 'a delay -> ?lax:bool -> constr option -> Id.t list -> (names_context * env) -> 
+  evar_map -> rel_context -> 'a glob_decl_g list
 
 val detype_closed_glob : ?lax:bool -> bool -> Id.t list -> env -> evar_map -> closed_glob_constr -> glob_constr
 
@@ -47,7 +51,7 @@ val lookup_name_as_displayed  : env -> evar_map -> constr -> Id.t -> int option
 val lookup_index_as_renamed : env -> evar_map -> constr -> int -> int option
 
 (* XXX: This is a hack and should go away *)
-val set_detype_anonymous : (?loc:Loc.t -> int -> glob_constr) -> unit
+val set_detype_anonymous : (?loc:Loc.t -> int -> Id.t) -> unit
 
 val force_wildcard : unit -> bool
 val synthetize_type : unit -> bool
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index b94228e75..c40a24e3b 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -23,8 +23,8 @@ let cases_predicate_names tml =
     | (tm,(na,None)) -> [na]
     | (tm,(na,Some (_,(_,nal)))) -> na::nal) tml)
 
-let mkGApp ?loc p t = CAst.make ?loc @@
-  match p.CAst.v with
+let mkGApp ?loc p t = DAst.make ?loc @@
+  match DAst.get p with
   | GApp (f,l) -> GApp (f,l@[t])
   | _          -> GApp (p,[t])
 
@@ -46,7 +46,7 @@ let case_style_eq s1 s2 = match s1, s2 with
   | RegularStyle, RegularStyle -> true
   | (LetStyle | IfStyle | LetPatternStyle | MatchStyle | RegularStyle), _ -> false
 
-let rec cases_pattern_eq { CAst.v = p1} { CAst.v = p2 } = match p1, p2 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 &&
@@ -98,7 +98,7 @@ let fix_kind_eq f k1 k2 = match k1, k2 with
 let instance_eq f (x1,c1) (x2,c2) =
   Id.equal x1 x2 && f c1 c2
 
-let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
+let mk_glob_constr_eq f c1 c2 = match DAst.get c1, DAst.get c2 with
   | GRef (gr1, _), GRef (gr2, _) -> eq_gr gr1 gr2
   | GVar id1, GVar id2 -> Id.equal id1 id2
   | GEvar (id1, arg1), GEvar (id2, arg2) ->
@@ -137,7 +137,7 @@ let mk_glob_constr_eq f { CAst.v = c1 } { CAst.v = c2 } = match c1, c2 with
 
 let rec glob_constr_eq c = mk_glob_constr_eq glob_constr_eq c
 
-let map_glob_constr_left_to_right f = CAst.map (function
+let map_glob_constr_left_to_right f = DAst.map (function
   | GApp (g,args) ->
       let comp1 = f g in
       let comp2 = Util.List.map_left f args in
@@ -186,7 +186,7 @@ let map_glob_constr = map_glob_constr_left_to_right
 
 let fold_return_type f acc (na,tyopt) = Option.fold_left f acc tyopt
 
-let fold_glob_constr f acc = CAst.with_val (function
+let fold_glob_constr f acc = DAst.with_val (function
   | GVar _ -> acc
   | GApp (c,args) -> List.fold_left f (f acc c) args
   | GLambda (_,_,b,c) | GProd (_,_,b,c) ->
@@ -217,7 +217,7 @@ let fold_glob_constr f acc = CAst.with_val (function
 let fold_return_type_with_binders f g v acc (na,tyopt) =
   Option.fold_left (f (Name.fold_right g na v)) acc tyopt
 
-let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
+let fold_glob_constr_with_binders g f v acc = DAst.(with_val (function
   | GVar _ -> acc
   | GApp (c,args) -> List.fold_left (f v) (f v acc c) args
   | GLambda (na,_,b,c) | GProd (na,_,b,c) ->
@@ -256,10 +256,9 @@ let fold_glob_constr_with_binders g f v acc = CAst.(with_val (function
 let iter_glob_constr f = fold_glob_constr (fun () -> f) ()
 
 let occur_glob_constr id =
-  let open CAst in
-  let rec occur barred acc = function
-    | { loc ; v = GVar id' } -> Id.equal id id'
-    | c ->
+  let rec occur barred acc c = match DAst.get c with
+    | GVar id' -> Id.equal id id'
+    | _ ->
        (* [g] looks if [id] appears in a binding position, in which
           case, we don't have to look in the corresponding subterm *)
        let g id' barred = barred || Id.equal id id' in
@@ -268,21 +267,20 @@ let occur_glob_constr id =
   occur false false
 
 let free_glob_vars =
-  let open CAst in
-  let rec vars bound vs = function
-    | { loc ; v = GVar id' } -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
-    | c -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
+  let rec vars bound vs c = match DAst.get c with
+    | GVar id' -> if Id.Set.mem id' bound then vs else Id.Set.add id' vs
+    | _ -> fold_glob_constr_with_binders Id.Set.add vars bound vs c in
   fun rt ->
     let vs = vars Id.Set.empty Id.Set.empty rt in
     Id.Set.elements vs
 
 let glob_visible_short_qualid c =
-  let rec aux acc = function
-    | { CAst.v = GRef (c,_) } ->
+  let rec aux acc c = match DAst.get c with
+    | GRef (c,_) ->
         let qualid = Nametab.shortest_qualid_of_global Id.Set.empty c in
         let dir,id = Libnames.repr_qualid  qualid in
         if DirPath.is_empty dir then id :: acc else acc
-    | c ->
+    | _ ->
         fold_glob_constr aux acc c
   in aux [] c
 
@@ -326,7 +324,7 @@ let map_tomatch_binders f ((c,(na,inp)) as x) : tomatch_tuple =
   if r == inp then x
   else c,(f na, r)
 
-let rec map_case_pattern_binders f = CAst.map (function
+let rec map_case_pattern_binders f = DAst.map (function
   | PatVar na as x ->
       let r = f na in
       if r == na then x
@@ -396,7 +394,9 @@ let rename_var l id =
     if List.exists (fun (_,id') -> Id.equal id id') l then raise UnsoundRenaming
     else id
 
-let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function
+let force c = DAst.make ?loc:c.CAst.loc (DAst.get c)
+
+let rec rename_glob_vars l c = force @@ DAst.map_with_loc (fun ?loc -> function
   | GVar id as r ->
       let id' = rename_var l id in
       if id == id' then r else GVar id'
@@ -436,13 +436,13 @@ let rec rename_glob_vars l c = CAst.map_with_loc (fun ?loc -> function
              test_na l na; (na,k,Option.map (rename_glob_vars l) bbd,rename_glob_vars l bty))) decls,
            Array.map (rename_glob_vars l) bs,
            Array.map (rename_glob_vars l) ts)
-  | _ -> (map_glob_constr (rename_glob_vars l) c).CAst.v
+  | _ -> DAst.get (map_glob_constr (rename_glob_vars l) c)
   ) c
 
 (**********************************************************************)
 (* Conversion from glob_constr to cases pattern, if possible            *)
 
-let rec cases_pattern_of_glob_constr na = CAst.map (function
+let rec cases_pattern_of_glob_constr na = DAst.map (function
   | GVar id ->
     begin match na with
     | Name _ ->
@@ -452,8 +452,12 @@ let rec cases_pattern_of_glob_constr na = CAst.map (function
     end
   | GHole (_,_,_) -> PatVar na
   | GRef (ConstructRef cstr,_) -> PatCstr (cstr,[],na)
-  | GApp ( { CAst.v = GRef (ConstructRef cstr,_) }, l) ->
+  | GApp (c, l) ->
+    begin match DAst.get c with
+    | GRef (ConstructRef cstr,_) ->
       PatCstr (cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+    | _ -> raise Not_found
+    end
   | _ -> raise Not_found
   )
 
@@ -469,7 +473,7 @@ let drop_local_defs typi args =
       | [], [] -> []
       | Rel.Declaration.LocalDef _ :: decls, pat :: args ->
          begin
-           match pat.CAst.v with
+           match DAst.get pat with
            | PatVar Anonymous -> aux decls args
            | _ -> raise Not_found (* The pattern is used, one cannot drop it *)
          end
@@ -487,21 +491,22 @@ let add_patterns_for_params_remove_local_defs (ind,j) l =
       let typi = mip.mind_nf_lc.(j-1) in
       let (_,typi) = decompose_prod_n_assum (Rel.length mib.mind_params_ctxt) typi in
       drop_local_defs typi l in
-  Util.List.addn nparams (CAst.make @@ PatVar Anonymous) l
+  Util.List.addn nparams (DAst.make @@ PatVar Anonymous) l
 
 (* Turn a closed cases pattern into a glob_constr *)
-let rec glob_constr_of_closed_cases_pattern_aux x = CAst.map_with_loc (fun ?loc -> function
+let rec glob_constr_of_closed_cases_pattern_aux x = DAst.map_with_loc (fun ?loc -> function
   | PatCstr (cstr,[],Anonymous) -> GRef (ConstructRef cstr,None)
   | PatCstr (cstr,l,Anonymous)  ->
-      let ref = CAst.make ?loc @@ GRef (ConstructRef cstr,None) in
+      let ref = DAst.make ?loc @@ GRef (ConstructRef cstr,None) in
       let l = add_patterns_for_params_remove_local_defs cstr l in
       GApp (ref, List.map glob_constr_of_closed_cases_pattern_aux l)
   | _ -> raise Not_found
   ) x
 
-let glob_constr_of_closed_cases_pattern = function
-  | { CAst.loc ; v = PatCstr (cstr,l,na) } ->
-      na,glob_constr_of_closed_cases_pattern_aux (CAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
+let glob_constr_of_closed_cases_pattern p = match DAst.get p with
+  | PatCstr (cstr,l,na) ->
+      let loc = p.CAst.loc in
+      na,glob_constr_of_closed_cases_pattern_aux (DAst.make ?loc @@ PatCstr (cstr,l,Anonymous))
   | _ ->
       raise Not_found
 
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index bd9e111f5..bacc8fbe4 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -11,21 +11,21 @@ open Glob_term
 
 (** Equalities *)
 
-val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
+val cases_pattern_eq : 'a cases_pattern_g -> 'a cases_pattern_g -> bool
 
 val cast_type_eq : ('a -> 'a -> bool) ->
   'a Misctypes.cast_type -> 'a Misctypes.cast_type -> bool
 
-val glob_constr_eq : glob_constr -> glob_constr -> bool
+val glob_constr_eq : 'a glob_constr_g -> 'a glob_constr_g -> bool
 
 (** Operations on [glob_constr] *)
 
-val cases_pattern_loc : cases_pattern -> Loc.t option
+val cases_pattern_loc : 'a cases_pattern_g -> Loc.t option
 
-val cases_predicate_names : tomatch_tuples -> Name.t list
+val cases_predicate_names : 'a tomatch_tuples_g -> Name.t list
 
 (** Apply one argument to a glob_constr *)
-val mkGApp : ?loc:Loc.t -> glob_constr -> glob_constr -> glob_constr
+val mkGApp : ?loc:Loc.t -> 'a glob_constr_g -> 'a glob_constr_g -> 'a glob_constr_g
 
 val map_glob_constr :
   (glob_constr -> glob_constr) -> glob_constr -> glob_constr
@@ -42,12 +42,12 @@ val mk_glob_constr_eq : (glob_constr -> glob_constr -> bool) ->
 val fold_glob_constr : ('a -> glob_constr -> 'a) -> 'a -> glob_constr -> 'a
 val fold_glob_constr_with_binders : (Id.t -> 'a -> 'a) -> ('a -> 'b -> glob_constr -> 'b) -> 'a -> 'b -> glob_constr -> 'b
 val iter_glob_constr : (glob_constr -> unit) -> glob_constr -> unit
-val occur_glob_constr : Id.t -> glob_constr -> bool
-val free_glob_vars : glob_constr -> Id.t list
+val occur_glob_constr : Id.t -> 'a glob_constr_g -> bool
+val free_glob_vars : 'a glob_constr_g -> Id.t list
 val bound_glob_vars : glob_constr -> Id.Set.t
 (* Obsolete *)
-val loc_of_glob_constr : glob_constr -> Loc.t option
-val glob_visible_short_qualid : glob_constr -> Id.t list
+val loc_of_glob_constr : 'a glob_constr_g -> Loc.t option
+val glob_visible_short_qualid : 'a glob_constr_g -> Id.t list
 
 (* Renaming free variables using a renaming map; fails with
    [UnsoundRenaming] if applying the renaming would introduce
@@ -57,7 +57,7 @@ val glob_visible_short_qualid : glob_constr -> Id.t list
 
 exception UnsoundRenaming
 val rename_var : (Id.t * Id.t) list -> Id.t -> Id.t
-val rename_glob_vars : (Id.t * Id.t) list -> glob_constr -> glob_constr
+val rename_glob_vars : (Id.t * Id.t) list -> 'a glob_constr_g -> 'a glob_constr_g
 
 (** [map_pattern_binders f m c] applies [f] to all the binding names
     in a pattern-matching expression ({!Glob_term.GCases}) represented
@@ -80,9 +80,9 @@ val map_pattern : (glob_constr -> glob_constr) ->
     @raise Not_found if translation is impossible *)
 val cases_pattern_of_glob_constr : Name.t -> glob_constr -> cases_pattern
 
-val glob_constr_of_closed_cases_pattern : cases_pattern -> Name.t * glob_constr
+val glob_constr_of_closed_cases_pattern : 'a cases_pattern_g -> Name.t * 'a glob_constr_g
 
-val add_patterns_for_params_remove_local_defs : constructor -> cases_pattern list -> cases_pattern list
+val add_patterns_for_params_remove_local_defs : constructor -> 'a cases_pattern_g list -> 'a cases_pattern_g list
 
 val ltac_interp_name : Glob_term.ltac_var_map -> Names.name -> Names.name
 val empty_lvar : Glob_term.ltac_var_map
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 5826cc135..3b3ad021e 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -326,7 +326,7 @@ let warn_cast_in_pattern =
   CWarnings.create ~name:"cast-in-pattern" ~category:"automation"
     (fun () -> Pp.strbrk "Casts are ignored in patterns")
 
-let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
+let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function
   | GVar id ->
       (try PRel (List.index Name.equal (Name id) vars)
        with Not_found -> PVar id)
@@ -335,11 +335,14 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
   | GRef (gr,_) ->
       PRef (canonical_gr gr)
   (* Hack to avoid rewriting a complete interpretation of patterns *)
-  | GApp ({ CAst.v = GPatVar (Evar_kinds.SecondOrderPatVar n) }, cl) ->
+  | GApp (c, cl) ->
+    begin match DAst.get c with
+    | GPatVar (Evar_kinds.SecondOrderPatVar n) ->
       metas := n::!metas; PSoApp (n, List.map (pat_of_raw metas vars) cl)
-  | GApp (c,cl) ->
+    | _ ->
       PApp (pat_of_raw metas vars c,
 	    Array.of_list (List.map (pat_of_raw metas vars) cl))
+    end
   | GLambda (na,bk,c1,c2) ->
       Name.iter (fun n -> metas := n::!metas) na;
       PLambda (na, pat_of_raw metas vars c1,
@@ -364,8 +367,8 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
       PIf (pat_of_raw metas vars c,
            pat_of_raw metas vars b1,pat_of_raw metas vars b2)
   | GLetTuple (nal,(_,None),b,c) ->
-      let mkGLambda na c = CAst.make ?loc @@
-	GLambda (na,Explicit, CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
+      let mkGLambda na c = DAst.make ?loc @@
+	GLambda (na,Explicit, DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None),c) in
       let c = List.fold_right mkGLambda nal c in
       let cip =
 	{ cip_style = LetStyle;
@@ -377,8 +380,12 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
       PCase (cip, PMeta None, pat_of_raw metas vars b,
              [0,tags,pat_of_raw metas vars c])
   | GCases (sty,p,[c,(na,indnames)],brs) ->
+      let get_ind p = match DAst.get p with 
+      | PatCstr((ind,_),_,_) -> Some ind
+      | _ -> None
+      in
       let get_ind = function
-	| (_,(_,[{ CAst.v = PatCstr((ind,_),_,_) }],_))::_ -> Some ind
+	| (_,(_,[p],_))::_ -> get_ind p
 	| _ -> None
       in
       let ind_tags,ind = match indnames with
@@ -391,8 +398,11 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
 	| Some p, Some (_,(_,nal)) ->
           let nvars = na :: List.rev nal @ vars in
           rev_it_mkPLambda nal (mkPLambda na (pat_of_raw metas nvars p))
-        | (None | Some { CAst.v = GHole _}), _ -> PMeta None
+        | None, _ -> PMeta None
 	| Some p, None ->
+          match DAst.get p with
+          | GHole _ -> PMeta None
+          | _ ->
             user_err ?loc  (strbrk "Clause \"in\" expected in patterns over \"match\" expressions with an explicit \"return\" clause.")
       in
       let info =
@@ -410,30 +420,36 @@ let rec pat_of_raw metas vars = CAst.with_loc_val (fun ?loc -> function
   )
 
 and pats_of_glob_branches loc metas vars ind brs =
-  let get_arg = function
-    | { CAst.v = PatVar na } ->
+  let get_arg p = match DAst.get p with
+    | PatVar na ->
       Name.iter (fun n -> metas := n::!metas) na;
       na
-    | { CAst.v = PatCstr(_,_,_) ; loc } -> err ?loc (Pp.str "Non supported pattern.")
+    | PatCstr(_,_,_) -> err ?loc:p.CAst.loc (Pp.str "Non supported pattern.")
   in
   let rec get_pat indexes = function
     | [] -> false, []
-    | [(_,(_,[{ CAst.v = PatVar Anonymous }], { CAst.v = GHole _}))] -> true, [] (* ends with _ => _ *)
-    | (_,(_,[{ CAst.v = PatCstr((indsp,j),lv,_) }],br)) :: brs ->
-      let () = match ind with
-      | Some sp when eq_ind sp indsp -> ()
+    | (loc',(_,[p], br)) :: brs ->
+      begin match DAst.get p, DAst.get br, brs with
+      | PatVar Anonymous, GHole _, [] ->
+        true, [] (* ends with _ => _ *)
+      | PatCstr((indsp,j),lv,_), _, _ ->
+        let () = match ind with
+        | Some sp when eq_ind sp indsp -> ()
+        | _ ->
+          err ?loc (Pp.str "All constructors must be in the same inductive type.")
+        in
+        if Int.Set.mem (j-1) indexes then
+          err ?loc
+            (str "No unique branch for " ++ int j ++ str"-th constructor.");
+        let lna = List.map get_arg lv in
+        let vars' = List.rev lna @ vars in
+        let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
+        let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
+        let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
+        ext, ((j-1, tags, pat) :: pats)
       | _ ->
-        err ?loc (Pp.str "All constructors must be in the same inductive type.")
-      in
-      if Int.Set.mem (j-1) indexes then
-	err ?loc
-          (str "No unique branch for " ++ int j ++ str"-th constructor.");
-      let lna = List.map get_arg lv in
-      let vars' = List.rev lna @ vars in
-      let pat = rev_it_mkPLambda lna (pat_of_raw metas vars' br) in
-      let ext,pats = get_pat (Int.Set.add (j-1) indexes) brs in
-      let tags = List.map (fun _ -> false) lv (* approximation, w/o let-in *) in
-      ext, ((j-1, tags, pat) :: pats)
+        err ?loc:loc' (Pp.str "Non supported pattern.")
+      end
     | (loc,(_,_,_)) :: _ -> err ?loc (Pp.str "Non supported pattern.")
   in
   get_pat Int.Set.empty brs
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 40b8bcad9..79d2c3333 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -572,7 +572,7 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
   let pretype = pretype k0 resolve_tc in
   let open Context.Rel.Declaration in
   let loc = t.CAst.loc in
-  match t.CAst.v with
+  match DAst.get t with
   | GRef (ref,u) ->
       inh_conv_coerce_to_tycon ?loc env evdref
 	(pretype_ref ?loc evdref env ref u)
@@ -1100,8 +1100,9 @@ and pretype_instance k0 resolve_tc env evdref lvar loc hyps evk update =
   Array.map_of_list snd subst
 
 (* [pretype_type valcon env evdref lvar c] coerces [c] into a type *)
-and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
-  | { loc; CAst.v = GHole (knd, naming, None) } ->
+and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar c = match DAst.get c with
+  | GHole (knd, naming, None) ->
+      let loc = loc_of_glob_constr c in
       let rec is_Type c = match EConstr.kind !evdref c with
       | Sort s ->
         begin match ESorts.kind !evdref s with
@@ -1134,7 +1135,7 @@ and pretype_type k0 resolve_tc valcon (env : ExtraEnv.t) evdref lvar = function
 	   let s = evd_comb0 (new_sort_variable univ_flexible_alg) evdref in
 	     { utj_val = e_new_evar env evdref ~src:(loc, knd) ~naming (mkSort s);
 	       utj_type = s})
-  | c ->
+  | _ ->
       let j = pretype k0 resolve_tc empty_tycon env evdref lvar c in
       let loc = loc_of_glob_constr c in
       let tj = evd_comb1 (Coercion.inh_coerce_to_sort ?loc env.ExtraEnv.env) evdref j in