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.

27 files changed, 395 insertions, 322 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 5a4c52456..fca7d9851 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -442,11 +442,11 @@ let cc_tactic depth additionnal_terms =
             let open Glob_term in
             let env = Proofview.Goal.env gl in
             let terms_to_complete = List.map (build_term_to_complete uf) (epsilons uf) 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 pr_missing (c, missing) =
-              let c = Detyping.detype ~lax:true false [] env sigma c in
+              let c = Detyping.detype Detyping.Now ~lax:true false [] env sigma c in
               let holes = List.init missing (fun _ -> hole) in
-              Printer.pr_glob_constr_env env (CAst.make @@ GApp (c, holes))
+              Printer.pr_glob_constr_env env (DAst.make @@ GApp (c, holes))
             in
 	    Feedback.msg_info
 	      (Pp.str "Goal is solvable by congruence but some arguments are missing.");
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 8cf5e8442..7087a195e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -34,10 +34,10 @@ type glob_context = (binder_type*glob_constr) list
 
 
 let rec solve_trivial_holes pat_as_term e =
-  match pat_as_term.CAst.v,e.CAst.v with
+  match DAst.get pat_as_term, DAst.get e with
   | GHole _,_ -> e
   | GApp(fp,argsp),GApp(fe,argse) when glob_constr_eq fp fe ->
-       CAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
+       DAst.make (GApp((solve_trivial_holes fp fe),List.map2 solve_trivial_holes argsp argse))
   | _,_ -> pat_as_term
                                               
 (*
@@ -361,7 +361,7 @@ let add_pat_variables pat typ env : Environ.env =
   let rec add_pat_variables env pat typ  : Environ.env =
     observe (str "new rel env := " ++ Printer.pr_rel_context_of env (Evd.from_env env));
 
-    match pat.CAst.v with
+    match DAst.get pat with
       | PatVar na -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
       | PatCstr(c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
@@ -411,7 +411,7 @@ let add_pat_variables pat typ env : Environ.env =
 
 
 
-let rec pattern_to_term_and_type env typ  = CAst.with_val (function
+let rec pattern_to_term_and_type env typ  = DAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar (Name id) ->
 	mkGVar id
@@ -434,7 +434,7 @@ let rec pattern_to_term_and_type env typ  = CAst.with_val (function
 	Array.to_list
 	  (Array.init
 	     (cst_narg - List.length patternl)
-	     (fun i -> Detyping.detype false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
+	     (fun i -> Detyping.detype Detyping.Now false [] env (Evd.from_env env) (EConstr.of_constr csta.(i)))
 	  )
       in
       let patl_as_term =
@@ -480,7 +480,7 @@ let rec pattern_to_term_and_type env typ  = CAst.with_val (function
 let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
   observe (str " Entering : " ++ Printer.pr_glob_constr rt);
   let open CAst in
-  match rt.v with
+  match DAst.get rt with
     | GRef _ | GVar _ | GEvar _ | GPatVar _ | GSort _  | GHole _ ->
 	(* do nothing (except changing type of course) *)
 	mk_result [] rt avoid
@@ -496,13 +496,13 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	    (mk_result [] [] avoid)
 	in
 	begin
-	  match f.v with
+	  match DAst.get f with
 	    | GLambda _  -> 
 		let rec aux t l = 
 		  match l with 
 		    | [] -> t
-		    | u::l -> CAst.make @@
-			match t.v with 
+		    | u::l -> DAst.make @@
+			match DAst.get t with 
 			  | GLambda(na,_,nat,b) -> 
 			      GLetIn(na,u,None,aux b l)
 			  | _ -> 
@@ -519,7 +519,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 		*)
 		let rt_as_constr,ctx = Pretyping.understand env (Evd.from_env env) rt in
 		let rt_typ = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr rt_as_constr) in
-		let res_raw_type = Detyping.detype false [] env (Evd.from_env env) rt_typ in
+		let res_raw_type = Detyping.detype Detyping.Now false [] env (Evd.from_env env) rt_typ in
 		let res = fresh_id args_res.to_avoid "_res" in
 		let new_avoid = res::args_res.to_avoid in
 		let res_rt = mkGVar res in
@@ -564,7 +564,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 			let new_b =
 			  replace_var_by_term
 			    id
-			    (CAst.make @@ GVar id)
+			    (DAst.make @@ GVar id)
 			    b
 			in
 			(Name new_id,new_b,new_avoid)
@@ -626,7 +626,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	   then the one corresponding to the value [t]
 	   and combine the two result
 	*)
-        let v = match typ with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
+        let v = match typ with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
 	let v_res = build_entry_lc env funnames avoid v in
 	let v_as_constr,ctx = Pretyping.understand env (Evd.from_env env) v in
 	let v_type = Typing.unsafe_type_of env (Evd.from_env env) (EConstr.of_constr v_as_constr) in
@@ -773,7 +773,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 			  Typing.unsafe_type_of env_with_pat_ids (Evd.from_env env) (EConstr.mkVar id)
 			in
 			let raw_typ_of_id =
-			  Detyping.detype false []
+			  Detyping.detype Detyping.Now false []
 			    env_with_pat_ids (Evd.from_env env) typ_of_id
 			in
 			mkGProd (Name id,raw_typ_of_id,acc))
@@ -819,7 +819,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	      (fun pat e typ_as_constr ->
 		 let this_pat_ids = ids_of_pat pat in
 		 let typ_as_constr = EConstr.of_constr typ_as_constr in
-		 let typ = Detyping.detype false [] new_env (Evd.from_env env) typ_as_constr in
+		 let typ = Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_as_constr in
 		 let pat_as_term = pattern_to_term pat in
                  (* removing trivial holes *) 
                  let pat_as_term = solve_trivial_holes pat_as_term e in 
@@ -833,7 +833,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 		      then (Prod (Name id),
 		      let typ_of_id = Typing.unsafe_type_of new_env (Evd.from_env env) (EConstr.mkVar id) in
 		      let raw_typ_of_id =
-			Detyping.detype false [] new_env (Evd.from_env env) typ_of_id
+			Detyping.detype Detyping.Now false [] new_env (Evd.from_env env) typ_of_id
 		      in
 		      raw_typ_of_id
 			   )::acc
@@ -875,15 +875,23 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
 	{ brl'_res with result = this_branch_res@brl'_res.result }
 
 
-let is_res id =
-  try
+let is_res r = match DAst.get r with
+| GVar id ->
+  begin try
     String.equal (String.sub (Id.to_string id) 0 4) "_res"
-  with Invalid_argument _ -> false
+  with Invalid_argument _ -> false end
+| _ -> false
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
 
+let is_gvar c = match DAst.get c with
+| GVar id -> true
+| _ -> false
 
 let same_raw_term rt1 rt2 = 
-  match CAst.(rt1.v, rt2.v) with 
+  match DAst.get rt1, DAst.get rt2 with 
     | GRef(r1,_), GRef (r2,_) -> Globnames.eq_gr r1 r2
     | GHole _, GHole _ -> true
     | _ -> false
@@ -917,23 +925,24 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
   observe (str "rebuilding : " ++ pr_glob_constr rt);
   let open Context.Rel.Declaration in
   let open CAst in
-  match rt.v with
+  match DAst.get rt with
     | GProd(n,k,t,b) ->
 	let not_free_in_t id = not (is_free_in id t) in
 	let new_crossed_types = t::crossed_types in
 	begin
-	  match t with
-	    | { v = GApp(({ v = GVar res_id } as res_rt),args') } when is_res res_id ->
+	  match DAst.get t with
+	    | GApp(res_rt ,args') when is_res res_rt ->
 		begin
-		  match args' with
-		    | { v = GVar this_relname }::args' ->
+                  let arg = List.hd args' in
+		  match DAst.get arg with
+		    | GVar this_relname ->
 			(*i The next call to mk_rel_id is
 			  valid since we are constructing the graph
 			  Ensures by: obvious
 			  i*)
 
 			let new_t =
-			  mkGApp(mkGVar(mk_rel_id this_relname),args'@[res_rt])
+			  mkGApp(mkGVar(mk_rel_id this_relname),List.tl args'@[res_rt])
 			in
 			let t',ctx = Pretyping.understand env (Evd.from_env env) new_t in
 			let new_env = Environ.push_rel (LocalAssum (n,t')) env in
@@ -948,9 +957,13 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    | _ -> (* the first args is the name of the function! *)
 			assert false
 		end
-	    | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty; { loc = loc3; v = GVar id};rt]) }
-		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
+	    | GApp(eq_as_ref,[ty; id ;rt])
+		when is_gvar id && is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref)  && n == Anonymous
 		  ->
+                let loc1 = rt.CAst.loc in
+                let loc2 = eq_as_ref.CAst.loc in
+                let loc3 = id.CAst.loc in
+                let id = match DAst.get id with GVar id -> id | _ -> assert false in
 		begin
 		  try
 		    observe (str "computing new type for eq : " ++ pr_glob_constr rt);
@@ -985,10 +998,10 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		    let params,arg' =
 		      ((Util.List.chop nparam args'))
 		    in
-		    let rt_typ = CAst.make @@
-		       GApp(CAst.make @@ GRef (Globnames.IndRef (fst ind),None),
+		    let rt_typ = DAst.make @@
+		       GApp(DAst.make @@ GRef (Globnames.IndRef (fst ind),None),
 			    (List.map
-			      (fun p -> Detyping.detype false []
+			      (fun p -> Detyping.detype Detyping.Now false []
 				 env (Evd.from_env env)
 				 (EConstr.of_constr p)) params)@(Array.to_list
 				      (Array.make
@@ -996,7 +1009,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 					 (mkGHole ()))))
 		    in
 		    let eq' =
-		      CAst.make ?loc:loc1 @@ GApp(CAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;CAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
+		      DAst.make ?loc:loc1 @@ GApp(DAst.make ?loc:loc2 @@GRef(jmeq,None),[ty;DAst.make ?loc:loc3 @@ GVar id;rt_typ;rt])
 		    in
 		    observe (str "computing new type for jmeq : " ++ pr_glob_constr eq');
 		    let eq'_as_constr,ctx = Pretyping.understand env (Evd.from_env env) eq' in
@@ -1015,12 +1028,12 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 				   match na with
 				     | Anonymous -> acc
 				     | Name id' ->
-					 (id',Detyping.detype false []
+					 (id',Detyping.detype Detyping.Now false []
 					    env
                                             (Evd.from_env env)
 					    arg)::acc
 				 else if isVar var_as_constr
-				 then (destVar var_as_constr,Detyping.detype false []
+				 then (destVar var_as_constr,Detyping.detype Detyping.Now false []
 					 env
                                          (Evd.from_env env)
 					 arg)::acc
@@ -1065,8 +1078,8 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		     mkGProd(n,t,new_b),id_to_exclude
 		     else new_b, Id.Set.add id id_to_exclude
 		  *)
-	    | { loc = loc1; v = GApp({ loc = loc2; v = GRef(eq_as_ref,_) },[ty;rt1;rt2]) }
-		when Globnames.eq_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
+	    | GApp(eq_as_ref,[ty;rt1;rt2])
+		when is_gr eq_as_ref (Lazy.force Coqlib.coq_eq_ref) && n == Anonymous
 		  ->
 	      begin
 		try 
@@ -1077,7 +1090,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		      List.fold_left 
 			(fun acc (lhs,rhs) -> 
 			  mkGProd(Anonymous,
-				  mkGApp(mkGRef(eq_as_ref),[mkGHole ();lhs;rhs]),acc)
+				  mkGApp(mkGRef(Lazy.force Coqlib.coq_eq_ref),[mkGHole ();lhs;rhs]),acc)
 			)
 			b
 			l
@@ -1135,14 +1148,14 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 		then
 		  new_b, Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
 		else
-		  CAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
+		  DAst.make @@ GProd(n,k,t,new_b),Id.Set.filter not_free_in_t id_to_exclude
 	    | _ -> anomaly (Pp.str "Should not have an anonymous function here.")
 		(* We have renamed all the anonymous functions during alpha_renaming phase *)
 
 	end
     | GLetIn(n,v,t,b) ->
 	begin
-          let t = match t with None -> v | Some t -> CAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
+          let t = match t with None -> v | Some t -> DAst.make ?loc:rt.loc @@ GCast (v,CastConv t) in
 	  let not_free_in_t id = not (is_free_in id t) in
 	  let evd = (Evd.from_env env) in
 	  let t',ctx = Pretyping.understand env evd t in
@@ -1158,7 +1171,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 	  match n with
 	    | Name id when Id.Set.mem id id_to_exclude && depth >= nb_args  ->
 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude)
-	    | _ -> CAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
+	    | _ -> DAst.make @@ GLetIn(n,t,None,new_b), (* HOPING IT WOULD WORK *)
 		Id.Set.filter not_free_in_t id_to_exclude
 	end
     | GLetTuple(nal,(na,rto),t,b) ->
@@ -1184,7 +1197,7 @@ let rec rebuild_cons env nb_args relname args crossed_types depth rt =
 (* 	    | Name id when Id.Set.mem id id_to_exclude ->  *)
 (* 		new_b,Id.Set.remove id (Id.Set.filter not_free_in_t id_to_exclude) *)
 (* 	    | _ -> *)
-	  CAst.make @@ GLetTuple(nal,(na,None),t,new_b),
+	  DAst.make @@ GLetTuple(nal,(na,None),t,new_b),
 		Id.Set.filter not_free_in_t (Id.Set.union id_to_exclude id_to_exclude')
 
 	end
@@ -1210,12 +1223,15 @@ let rebuild_cons env nb_args relname args crossed_types rt =
 
    TODO: Find a valid way to deal with implicit arguments here!
 *)
-let rec compute_cst_params relnames params gt = CAst.with_val (function
+let rec compute_cst_params relnames params gt = DAst.with_val (function
   | GRef _ | GVar _ | GEvar _ | GPatVar _ -> params
-  | GApp({ CAst.v = GVar relname' },rtl) when Id.Set.mem relname' relnames ->
-      compute_cst_params_from_app [] (params,rtl)
   | GApp(f,args) ->
+    begin match DAst.get f with
+    | GVar relname' when Id.Set.mem relname' relnames ->
+      compute_cst_params_from_app [] (params,args)
+    | _ ->
       List.fold_left (compute_cst_params relnames) params (f::args)
+    end
   | GLambda(_,_,t,b) | GProd(_,_,t,b) | GLetTuple(_,_,t,b) ->
       let t_params = compute_cst_params relnames params t in
       compute_cst_params relnames t_params b
@@ -1232,10 +1248,10 @@ let rec compute_cst_params relnames params gt = CAst.with_val (function
       raise (UserError(Some "compute_cst_params", str "Not handled case"))
   ) gt
 and compute_cst_params_from_app acc (params,rtl) =
+  let is_gid id c = match DAst.get c with GVar id' -> Id.equal id id' | _ -> false in
   match params,rtl with
     | _::_,[] -> assert false (* the rel has at least nargs + 1 arguments ! *)
-    | ((Name id,_,None) as param)::params', { CAst.v = GVar id' }::rtl'
-	when Id.compare id id' == 0 ->
+    | ((Name id,_,None) as param)::params', c::rtl' when is_gid id c ->
 	compute_cst_params_from_app (param::acc) (params',rtl')
     | _  -> List.rev acc
 
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 003bb4e30..02ee56ac5 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -10,36 +10,36 @@ open Misctypes
    Some basic functions to rebuild glob_constr
    In each of them the location is Loc.ghost
 *)
-let mkGRef ref          = CAst.make @@ GRef(ref,None)
-let mkGVar id           = CAst.make @@ GVar(id)
-let mkGApp(rt,rtl)      = CAst.make @@ GApp(rt,rtl)
-let mkGLambda(n,t,b)    = CAst.make @@ GLambda(n,Explicit,t,b)
-let mkGProd(n,t,b)      = CAst.make @@ GProd(n,Explicit,t,b)
-let mkGLetIn(n,b,t,c)   = CAst.make @@ GLetIn(n,b,t,c)
-let mkGCases(rto,l,brl) = CAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
-let mkGSort s           = CAst.make @@ GSort(s)
-let mkGHole ()          = CAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
-let mkGCast(b,t)        = CAst.make @@ GCast(b,CastConv t)
+let mkGRef ref          = DAst.make @@ GRef(ref,None)
+let mkGVar id           = DAst.make @@ GVar(id)
+let mkGApp(rt,rtl)      = DAst.make @@ GApp(rt,rtl)
+let mkGLambda(n,t,b)    = DAst.make @@ GLambda(n,Explicit,t,b)
+let mkGProd(n,t,b)      = DAst.make @@ GProd(n,Explicit,t,b)
+let mkGLetIn(n,b,t,c)   = DAst.make @@ GLetIn(n,b,t,c)
+let mkGCases(rto,l,brl) = DAst.make @@ GCases(Term.RegularStyle,rto,l,brl)
+let mkGSort s           = DAst.make @@ GSort(s)
+let mkGHole ()          = DAst.make @@ GHole(Evar_kinds.BinderType Anonymous,Misctypes.IntroAnonymous,None)
+let mkGCast(b,t)        = DAst.make @@ GCast(b,CastConv t)
 
 (*
   Some basic functions to decompose glob_constrs
   These are analogous to the ones constrs
 *)
 let glob_decompose_prod =
-  let rec glob_decompose_prod args = function
-  | { CAst.v = GProd(n,k,t,b) } ->
+  let rec glob_decompose_prod args c = match DAst.get c with
+  | GProd(n,k,t,b) ->
       glob_decompose_prod ((n,t)::args) b
-  | rt -> args,rt
+  | _ -> args,c
   in
   glob_decompose_prod []
 
 let glob_decompose_prod_or_letin =
-  let rec glob_decompose_prod args = function
-  | { CAst.v = GProd(n,k,t,b) } ->
+  let rec glob_decompose_prod args rt = match DAst.get rt with
+  | GProd(n,k,t,b) ->
       glob_decompose_prod ((n,None,Some t)::args) b
-  | { CAst.v = GLetIn(n,b,t,c) } ->
+  | GLetIn(n,b,t,c) ->
       glob_decompose_prod ((n,Some b,t)::args) c
-  | rt -> args,rt
+  | _ -> args,rt
   in
   glob_decompose_prod []
 
@@ -58,10 +58,10 @@ let glob_decompose_prod_n n =
   let rec glob_decompose_prod i args c =
     if i<=0 then args,c
     else
-      match c with
-	| { CAst.v = GProd(n,_,t,b) } ->
+      match DAst.get c with
+	| GProd(n,_,t,b) ->
 	    glob_decompose_prod (i-1) ((n,t)::args) b
-	| rt -> args,rt
+	| _ -> args,c
   in
   glob_decompose_prod n []
 
@@ -70,12 +70,12 @@ let glob_decompose_prod_or_letin_n n =
   let rec glob_decompose_prod i args c =
     if i<=0 then args,c
     else
-      match c with
-	| { CAst.v = GProd(n,_,t,b) } ->
+      match DAst.get c with
+	| GProd(n,_,t,b) ->
 	    glob_decompose_prod (i-1) ((n,None,Some t)::args) b
-	| { CAst.v = GLetIn(n,b,t,c) } ->
+	| GLetIn(n,b,t,c) ->
 	    glob_decompose_prod (i-1) ((n,Some b,t)::args) c
-	| rt -> args,rt
+	| _ -> args,c
   in
   glob_decompose_prod n []
 
@@ -83,10 +83,10 @@ let glob_decompose_prod_or_letin_n n =
 let glob_decompose_app =
   let rec decompose_rapp acc rt =
 (*     msgnl (str "glob_decompose_app on : "++ Printer.pr_glob_constr rt); *)
-    match rt with
-    | { CAst.v = GApp(rt,rtl) } ->
+    match DAst.get rt with
+    | GApp(rt,rtl) ->
 	decompose_rapp (List.fold_left (fun y x -> x::y) acc rtl) rt
-    | rt -> rt,List.rev acc
+    | _ -> rt,List.rev acc
   in
   decompose_rapp []
 
@@ -120,7 +120,7 @@ let remove_name_from_mapping mapping na =
 
 let change_vars =
   let rec change_vars mapping rt =
-    CAst.map_with_loc (fun ?loc -> function
+    DAst.map_with_loc (fun ?loc -> function
       | GRef _ as x -> x
       | GVar id ->
 	  let new_id =
@@ -191,15 +191,15 @@ let change_vars =
 
 let rec alpha_pat excluded pat =
   let loc = pat.CAst.loc in
-  match pat.CAst.v with
+  match DAst.get pat with
     | PatVar Anonymous ->
 	let new_id = Indfun_common.fresh_id excluded "_x" in
-	(CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
+	(DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),Id.Map.empty
     | PatVar(Name id) ->
 	if Id.List.mem id excluded
 	then
 	  let new_id = Namegen.next_ident_away id excluded in
-	  (CAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
+	  (DAst.make ?loc @@ PatVar(Name new_id)),(new_id::excluded),
 	(Id.Map.add id new_id Id.Map.empty)
 	else pat, excluded,Id.Map.empty
     | PatCstr(constr,patl,na) ->
@@ -219,7 +219,7 @@ let rec alpha_pat excluded pat =
 	    ([],new_excluded,map)
 	    patl
 	in
-        (CAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
+        (DAst.make ?loc @@ PatCstr(constr,List.rev new_patl,new_na)),new_excluded,new_map
 
 let alpha_patl excluded patl  =
   let patl,new_excluded,map =
@@ -238,7 +238,7 @@ let alpha_patl excluded patl  =
 
 let raw_get_pattern_id pat acc =
   let rec get_pattern_id pat =
-    match pat.CAst.v with
+    match DAst.get pat with
       | PatVar(Anonymous) -> assert false
       | PatVar(Name id) ->
 	  [id]
@@ -257,8 +257,8 @@ let get_pattern_id pat = raw_get_pattern_id pat []
 
 let rec alpha_rt excluded rt =
   let loc = rt.CAst.loc in
-  let new_rt = CAst.make ?loc @@
-    match rt.CAst.v with
+  let new_rt = DAst.make ?loc @@
+    match DAst.get rt with
       | GRef _ | GVar _ | GEvar _ | GPatVar _ as rt -> rt
       | GLambda(Anonymous,k,t,b) ->
 	  let new_id = Namegen.next_ident_away (Id.of_string "_x") excluded in
@@ -377,7 +377,7 @@ and alpha_br excluded (loc,(ids,patl,res)) =
    [is_free_in id rt] checks if [id] is a free variable in [rt]
 *)
 let is_free_in id =
-  let rec is_free_in x = CAst.with_loc_val (fun ?loc -> function
+  let rec is_free_in x = DAst.with_loc_val (fun ?loc -> function
     | GRef _ ->  false
     | GVar id' -> Id.compare id' id == 0
     | GEvar _ -> false
@@ -421,7 +421,7 @@ let is_free_in id =
 
 
 
-let rec pattern_to_term pt = CAst.with_val (function
+let rec pattern_to_term pt = DAst.with_val (function
   | PatVar Anonymous -> assert false
   | PatVar(Name id) ->
 	mkGVar id
@@ -448,8 +448,8 @@ let rec pattern_to_term pt = CAst.with_val (function
 
 
 let replace_var_by_term x_id term =
-  let rec replace_var_by_pattern x = CAst.map (function
-      | GVar id when Id.compare id x_id == 0 -> term.CAst.v
+  let rec replace_var_by_pattern x = DAst.map (function
+      | GVar id when Id.compare id x_id == 0 -> DAst.get term
       | GRef _
       | GVar _
       | GEvar _
@@ -522,11 +522,10 @@ exception NotUnifiable
 
 let rec are_unifiable_aux  = function
   | [] -> ()
-  | eq::eqs ->
-      let open CAst in
-      match eq with
-	 | { v = PatVar _ },_ | _, { v = PatVar _ } -> are_unifiable_aux eqs
-	 | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
+  | (l, r) ::eqs ->
+      match DAst.get l, DAst.get r with
+	 | PatVar _ ,_ | _, PatVar _-> are_unifiable_aux eqs
+	 | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
 	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
@@ -545,11 +544,10 @@ let are_unifiable pat1 pat2 =
 
 let rec eq_cases_pattern_aux  = function
   | [] -> ()
-  | eq::eqs ->
-      let open CAst in
-      match eq with
-	 | { v = PatVar _ }, { v = PatVar _ } -> eq_cases_pattern_aux eqs
-	 | { v = PatCstr(constructor1,cpl1,_) }, { v = PatCstr(constructor2,cpl2,_) } ->
+  | (l, r) ::eqs ->
+      match DAst.get l, DAst.get r with
+	 | PatVar _, PatVar _ -> eq_cases_pattern_aux eqs
+	 | PatCstr(constructor1,cpl1,_), PatCstr(constructor2,cpl2,_) ->
 	     if not (eq_constructor constructor2 constructor1)
 	     then raise NotUnifiable
 	     else
@@ -569,7 +567,7 @@ let eq_cases_pattern pat1 pat2 =
 
 
 let ids_of_pat =
-  let rec ids_of_pat ids = CAst.with_val (function
+  let rec ids_of_pat ids = DAst.with_val (function
     | PatVar Anonymous -> ids
     | PatVar(Name id) -> Id.Set.add id ids
     | PatCstr(_,patl,_) -> List.fold_left ids_of_pat ids patl
@@ -583,9 +581,9 @@ let id_of_name = function
 
 (* TODO: finish Rec caes *)
 let ids_of_glob_constr c =
-  let rec ids_of_glob_constr acc {loc; CAst.v = c} =
+  let rec ids_of_glob_constr acc c =
     let idof = id_of_name in
-    match c with
+    match DAst.get c with
       | GVar id -> id::acc
       | GApp (g,args) ->
           ids_of_glob_constr [] g @ List.flatten (List.map (ids_of_glob_constr []) args) @ acc
@@ -610,7 +608,7 @@ let ids_of_glob_constr c =
 
 
 let zeta_normalize =
-  let rec zeta_normalize_term x = CAst.map (function
+  let rec zeta_normalize_term x = DAst.map (function
       | GRef _
       | GVar _
       | GEvar _
@@ -632,9 +630,9 @@ let zeta_normalize =
 		zeta_normalize_term b
 		 )
       | GLetIn(Name id,def,typ,b) ->
-	  (zeta_normalize_term (replace_var_by_term id def b)).CAst.v
+	  DAst.get (zeta_normalize_term (replace_var_by_term id def b))
       | GLetIn(Anonymous,def,typ,b) ->
-          (zeta_normalize_term b).CAst.v
+          DAst.get (zeta_normalize_term b)
       | GLetTuple(nal,(na,rto),def,b) ->
 	  GLetTuple(nal,
 		    (na,Option.map zeta_normalize_term rto),
@@ -670,19 +668,19 @@ let zeta_normalize =
 
 let expand_as =
 
-  let rec add_as map ({loc; CAst.v = pat } as rt) =
-    match pat with
+  let rec add_as map rt =
+    match DAst.get rt with
       | PatVar _ -> map
       | PatCstr(_,patl,Name id) ->
 	  Id.Map.add id (pattern_to_term rt) (List.fold_left add_as map patl)
       | PatCstr(_,patl,_) -> List.fold_left add_as map patl
   in
-  let rec expand_as map = CAst.map (function
+  let rec expand_as map = DAst.map (function
       | GRef _ | GEvar _ | GPatVar _ | GSort _ | GHole _ as rt -> rt
       | GVar id as rt ->
 	  begin
 	    try
-	      (Id.Map.find id map).CAst.v
+	      DAst.get (Id.Map.find id map)
 	    with Not_found -> rt
 	  end
       | GApp(f,args) -> GApp(expand_as map f,List.map (expand_as map) args)
@@ -723,7 +721,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
 
   (* then we map [rt] to replace the implicit holes by their values *)
   let rec change rt =
-    match rt.CAst.v with
+    match DAst.get rt with
     | GHole(ImplicitArg(grk,pk,bk),_,_) -> (* we only want to deal with implicit arguments *)
        (
          try (* we scan the new evar map to find the evar corresponding to this hole (by looking the source *)
@@ -743,7 +741,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
            match evi.evar_body with
            | Evar_defined c ->
            (* we just have to lift the solution in glob_term *)
-              Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+              Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c))
            | Evar_empty -> rt (* the hole was not solved : we do nothing *)
        )
     | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
@@ -765,7 +763,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
                 match evi.evar_body with
                 | Evar_defined c ->
                    (* we just have to lift the solution in glob_term *)
-                   Detyping.detype false [] env ctx (EConstr.of_constr (f c))
+                   Detyping.detype Detyping.Now false [] env ctx (EConstr.of_constr (f c))
                 | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
          in 
          res
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 8769f5668..dab094f91 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -191,7 +191,7 @@ let error msg = user_err Pp.(str msg)
 let is_rec names =
   let names = List.fold_right Id.Set.add names Id.Set.empty in
   let check_id id names =  Id.Set.mem id names in
-  let rec lookup names gt = match gt.CAst.v with
+  let rec lookup names gt = match DAst.get gt with
     | GVar(id) -> check_id id names
     | GRef _ | GEvar _ | GPatVar _ | GSort _ |  GHole _ -> false
     | GCast(b,_) -> lookup names b
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index f4f9ba2bb..5f4d514f3 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -66,7 +66,7 @@ let chop_rlambda_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match rt.CAst.v with
+	match DAst.get rt with
 	  | Glob_term.GLambda(name,k,t,b) -> chop_lambda_n ((name,t,None)::acc) (n-1) b
 	  | Glob_term.GLetIn(name,v,t,b) -> chop_lambda_n ((name,v,t)::acc) (n-1) b
 	  | _ ->
@@ -80,7 +80,7 @@ let chop_rprod_n  =
       if n == 0
       then List.rev acc,rt
       else
-	match rt.CAst.v with
+	match DAst.get rt with
 	  | Glob_term.GProd(name,k,t,b) -> chop_prod_n ((name,t)::acc) (n-1) b
 	  | _ -> raise (CErrors.UserError(Some "chop_rprod_n",str "chop_rprod_n: Not enough products"))
   in
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 3ae922190..96200a98a 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -64,8 +64,8 @@ let string_of_name = id_of_name %> Id.to_string
 
 (** [isVarf f x] returns [true] if term [x] is of the form [(Var f)]. *)
 let isVarf f x =
-    match x with
-      | { CAst.v = GVar x } -> Id.equal x f
+    match DAst.get x with
+      | GVar x -> Id.equal x f
       | _ -> false
 
 (** [ident_global_exist id] returns true if identifier [id] is linked
@@ -491,38 +491,38 @@ exception NoMerge
 
 let rec merge_app c1 c2 id1 id2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match CAst.(c1.v, c2.v) with
+  match DAst.get c1, DAst.get c2 with
     | GApp(f1, arr1), GApp(f2,arr2) when isVarf id1 f1 && isVarf id2 f2 ->
         let _ = prstr "\nICI1!\n" in
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        CAst.make @@ GApp ((CAst.make @@ GVar shift.ident) , args)
+        DAst.make @@ GApp ((DAst.make @@ GVar shift.ident) , args)
     | GApp(f1, arr1), GApp(f2,arr2)  -> raise NoMerge
     | GLetIn(nme,bdy,typ,trm) , _ ->
         let _ = prstr "\nICI2!\n" in
         let newtrm = merge_app trm c2 id1 id2 shift filter_shift_stable in
-        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
+        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _, GLetIn(nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3!\n" in
         let newtrm = merge_app c1 trm id1 id2 shift filter_shift_stable in
-        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
+        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4!\n" in
            raise NoMerge
 
 let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
   let lnk = Array.append shift.lnk1 shift.lnk2 in
-  match CAst.(c1.v, c2.v) with
+  match DAst.get c1, DAst.get c2 with
     | GApp(f1, arr1), GApp(f2,arr2) ->
         let args = filter_shift_stable lnk (arr1 @ arr2) in
-        CAst.make @@ GApp (CAst.make @@ GVar shift.ident, args)
+        DAst.make @@ GApp (DAst.make @@ GVar shift.ident, args)
           (* FIXME: what if the function appears in the body of the let? *)
     | GLetIn(nme,bdy,typ,trm) , _ ->
       let _ = prstr "\nICI2 '!\n" in
         let newtrm = merge_app_unsafe trm c2 shift filter_shift_stable in
-        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
+        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _, GLetIn(nme,bdy,typ,trm) ->
         let _ = prstr "\nICI3 '!\n" in
         let newtrm = merge_app_unsafe c1 trm shift filter_shift_stable in
-        CAst.make @@ GLetIn(nme,bdy,typ,newtrm)
+        DAst.make @@ GLetIn(nme,bdy,typ,newtrm)
     | _ -> let _ = prstr "\nICI4 '!\n" in raise NoMerge
 
 
@@ -533,16 +533,18 @@ let rec merge_app_unsafe c1 c2 shift filter_shift_stable =
 let rec merge_rec_hyps shift accrec
     (ltyp:(Name.t * glob_constr option * glob_constr option) list)
     filter_shift_stable : (Name.t * glob_constr option * glob_constr option) list =
+  let is_app c = match DAst.get c with GApp _ -> true | _ -> false in
   let mergeonehyp t reldecl =
     match reldecl with
-      | (nme,x,Some ({ CAst.v = GApp(i,args)} as ind))
+      | (nme,x,Some ind) when is_app ind
         -> nme,x, Some (merge_app_unsafe ind t shift filter_shift_stable)
       | (nme,Some _,None) -> error "letins with recursive calls not treated yet"
       | (nme,None,Some _) -> assert false
       | (nme,None,None) | (nme,Some _,Some _) -> assert false in
+  let is_app c = match DAst.get c with GApp (f, _) -> isVarf ind2name f | _ -> false in
   match ltyp with
     | [] -> []
-    | (nme,None,Some ({ CAst. v = GApp(f, largs) } as t)) :: lt when isVarf ind2name f ->
+    | (nme,None,Some t) :: lt when is_app t ->
         let rechyps = List.map (mergeonehyp t) accrec in
         rechyps @ merge_rec_hyps shift accrec lt filter_shift_stable
     | e::lt -> e :: merge_rec_hyps shift accrec lt filter_shift_stable
@@ -553,12 +555,13 @@ let build_suppl_reccall (accrec:(Name.t * glob_constr) list) concl2 shift =
 
 
 let find_app (nme:Id.t) ltyp =
+  let is_app c = match DAst.get c with GApp (f, _) -> isVarf nme f | _ -> false in
   try
     ignore
       (List.map
           (fun x ->
             match x with
-              | _,None,Some { CAst.v = GApp(f,_)} when isVarf nme f -> raise (Found 0)
+              | _,None,Some c when is_app c -> raise (Found 0)
               | _ -> ())
           ltyp);
     false
@@ -617,7 +620,7 @@ let rec merge_types shift accrec1
 
           rechyps , concl
       | (nme,None, Some t1)as e ::lt1 ->
-          (match t1.CAst.v with
+          (match DAst.get t1 with
             | GApp(f,carr) when isVarf ind1name f ->
                 merge_types shift (e::accrec1) lt1 concl1 ltyp2 concl2
             | _ ->
@@ -764,7 +767,7 @@ let merge_inductive_body (shift:merge_infos) avoid (oib1:one_inductive_body)
     (* first replace rel 1 by a varname *)
     let substindtyp = substitterm 0 (mkRel 1) (mkVar nme) typ in
     let substindtyp = EConstr.of_constr substindtyp in
-    Detyping.detype false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
+    Detyping.detype Detyping.Now false (Id.Set.elements avoid) (Global.env()) Evd.empty substindtyp in
   let lcstr1: glob_constr list =
     Array.to_list (Array.map (mkrawcor ind1name avoid) oib1.mind_user_lc) in
   (* add  to avoid all indentifiers of lcstr1 *)
@@ -848,8 +851,8 @@ let mkProd_reldecl (rdecl:Context.Rel.Declaration.t) (t2:glob_constr) =
   match rdecl with
     | LocalAssum (nme,t) ->
         let t = EConstr.of_constr t in
-        let traw = Detyping.detype false [] (Global.env()) Evd.empty t in
-        CAst.make @@ GProd (nme,Explicit,traw,t2)
+        let traw = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in
+        DAst.make @@ GProd (nme,Explicit,traw,t2)
     | LocalDef _ -> assert false
 
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d3eccb58d..41a10cba3 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -190,15 +190,15 @@ let (value_f:Term.constr list -> global_reference -> Term.constr) =
     in
     let env = Environ.push_rel_context context (Global.env ()) in
     let glob_body =
-      CAst.make @@
+      DAst.make @@
        GCases
 	(RegularStyle,None,
-	 [CAst.make @@ GApp(CAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> CAst.make @@ GVar x_id) rev_x_id_l),
+	 [DAst.make @@ GApp(DAst.make @@ GRef(fterm,None), List.rev_map (fun x_id -> DAst.make @@ GVar x_id) rev_x_id_l),
 	  (Anonymous,None)],
-	 [Loc.tag ([v_id], [CAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
-			   [CAst.make @@ PatVar(Name v_id); CAst.make @@ PatVar Anonymous],
+	 [Loc.tag ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
+			   [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous],
                            Anonymous)],
-	    CAst.make @@ GVar v_id)])
+	    DAst.make @@ GVar v_id)])
     in
     let body = fst (understand env (Evd.from_env env) glob_body)(*FIXME*) in
     it_mkLambda_or_LetIn body context
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index b847aadf2..99e444010 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -626,19 +626,19 @@ END
 let subst_var_with_hole occ tid t = 
   let occref = if occ > 0 then ref occ else Find_subterm.error_invalid_occurrence [occ] in
   let locref = ref 0 in
-  let rec substrec = function
-    | { CAst.v = GVar id } as x -> 
+  let rec substrec x = match DAst.get x with
+    | GVar id ->
         if Id.equal id tid 
         then
 	  (decr occref;
 	   if Int.equal !occref 0 then x
            else
 	     (incr locref;
-              CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+              DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	      GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),
                      Misctypes.IntroAnonymous, None)))
         else x
-    | c -> map_glob_constr_left_to_right substrec c in
+    | _ -> map_glob_constr_left_to_right substrec x in
   let t' = substrec t
   in
   if !occref > 0 then Find_subterm.error_invalid_occurrence [occ] else t'
@@ -646,15 +646,15 @@ let subst_var_with_hole occ tid t =
 let subst_hole_with_term occ tc t =
   let locref = ref 0 in
   let occref = ref occ in
-  let rec substrec = function
-    | { CAst.v = GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) } ->
+  let rec substrec c = match DAst.get c with
+    | GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s) ->
         decr occref;
         if Int.equal !occref 0 then tc
         else
 	  (incr locref;
-           CAst.make ~loc:(Loc.make_loc (!locref,0)) @@
+           DAst.make ~loc:(Loc.make_loc (!locref,0)) @@
 	   GHole (Evar_kinds.QuestionMark(Evar_kinds.Define true,Anonymous),Misctypes.IntroAnonymous,s))
-    | c -> map_glob_constr_left_to_right substrec c
+    | _ -> map_glob_constr_left_to_right substrec c
   in
   substrec t
 
@@ -666,8 +666,8 @@ let hResolve id c occ t =
   let env = Termops.clear_named_body id (Proofview.Goal.env gl) in
   let concl = Proofview.Goal.concl gl in
   let env_ids = Termops.ids_of_context env in
-  let c_raw = Detyping.detype true env_ids env sigma c in
-  let t_raw = Detyping.detype true env_ids env sigma t in
+  let c_raw = Detyping.detype Detyping.Now true env_ids env sigma c in
+  let t_raw = Detyping.detype Detyping.Now true env_ids env sigma t in
   let rec resolve_hole t_hole =
     try 
       Pretyping.understand env sigma t_hole
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4
index c874f8d5a..c22e68323 100644
--- a/plugins/ltac/g_rewrite.ml4
+++ b/plugins/ltac/g_rewrite.ml4
@@ -123,7 +123,7 @@ END
 
 let clsubstitute o c =
   Proofview.Goal.enter begin fun gl ->
-  let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in
+  let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in
   let hyps = Tacmach.New.pf_ids_of_hyps gl in
     Tacticals.New.tclMAP
       (fun cl ->
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index cb7d9b9c0..f4e3ba633 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1040,7 +1040,7 @@ type 'a extra_genarg_printer =
   let strip_prod_binders_glob_constr n (ty,_) =
     let rec strip_ty acc n ty =
       if Int.equal n 0 then (List.rev acc, (ty,None)) else
-        match ty.CAst.v with
+        match DAst.get ty with
             Glob_term.GProd(na,Explicit,a,b) ->
               strip_ty (([Loc.tag na],(a,None))::acc) (n-1) b
           | _ -> user_err Pp.(str "Cannot translate fix tactic: not enough products") in
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 0554d4364..fc6ee6aab 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -106,12 +106,12 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      (CAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
+      (DAst.make @@ GVar id), Some (CAst.make @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      (CAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
+      (DAst.make @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
-      CAst.make @@ GRef (locate_global_with_alias lqid,None), 
+      DAst.make @@ GRef (locate_global_with_alias lqid,None), 
 	if strict then None else Some (CAst.make @@ CRef (r,None))
 
 (* Internalize an isolated reference in position of tactic *)
@@ -264,9 +264,10 @@ let intern_destruction_arg ist = function
   | clear,ElimOnIdent (loc,id) ->
       if !strict_check then
 	(* If in a defined tactic, no intros-until *)
-	match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
-	| {loc; CAst.v = GVar id}, _ -> clear,ElimOnIdent (loc,id)
-	| c -> clear,ElimOnConstr (c,NoBindings)
+	let c, p = intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) in
+	match DAst.get c with
+	| GVar id -> clear,ElimOnIdent (c.CAst.loc,id)
+	| _ -> clear,ElimOnConstr ((c, p), NoBindings)
       else
 	clear,ElimOnIdent (loc,id)
 
@@ -348,7 +349,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
         ltac_extra = ist.extra;
       } in
       let c = Constrintern.interp_reference sign r in
-      match c.CAst.v with
+      match DAst.get c with
       | GRef (r,None) ->
           Inl (ArgArg (evaluable_of_global_reference ist.genv r,None))
       | GVar id ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 2a1e2b682..8fa95ffb0 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -679,8 +679,8 @@ let interp_typed_pattern ist env sigma (_,c,_) =
 (* Interprets a constr expression *)
 let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l =
   let try_expand_ltac_var sigma x =
-    try match dest_fun x with
-    | { CAst.v = GVar id }, _ ->
+    try match DAst.get (fst (dest_fun x)) with
+    | GVar id ->
       let v = Id.Map.find id ist.lfun in
       sigma, List.map inj_fun (coerce_to_constr_list env v)
     | _ ->
@@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
+          let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
           let f env sigma =
             let (sigma,c) = interp_open_constr ist env sigma c in
             (sigma, (c,NoBindings))
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index 0f996c65a..d0fe1f957 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -131,7 +131,7 @@ let closed_term_ast l =
   let l = List.map (fun gr -> ArgArg(Loc.tag gr)) l in
   TacFun([Name(Id.of_string"t")],
   TacML(Loc.tag (tacname,
-  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (CAst.make @@ GVar(Id.of_string"t"),None));
+  [TacGeneric (Genarg.in_gen (Genarg.glbwit Stdarg.wit_constr) (DAst.make @@ GVar(Id.of_string"t"),None));
    TacGeneric (Genarg.in_gen (Genarg.glbwit (Genarg.wit_list Stdarg.wit_ref)) l)])))
 (*
 let _ = add_tacdef false ((Loc.ghost,Id.of_string"ring_closed_term"
diff --git a/plugins/ssr/ssrbwd.ml b/plugins/ssr/ssrbwd.ml
index cc0e86684..c29a1fe7c 100644
--- a/plugins/ssr/ssrbwd.ml
+++ b/plugins/ssr/ssrbwd.ml
@@ -42,10 +42,10 @@ let interp_agen ist gl ((goclr, _), (k, gc as c)) (clr, rcs) =
   | Some ghyps ->
     let clr' = snd (interp_hyps ist gl ghyps) @ clr in
     if k <> xNoFlag then clr', rcs' else
-    let open CAst in
-    match rc with
-    | { loc; v = GVar id } when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
-    | { loc; v = GRef (VarRef id, _) } when not_section_id id ->
+    let loc = rc.CAst.loc in
+    match DAst.get rc with
+    | GVar id when not_section_id id -> SsrHyp (Loc.tag ?loc id) :: clr', rcs'
+    | GRef (VarRef id, _) when not_section_id id ->
         SsrHyp (Loc.tag ?loc id) :: clr', rcs'
     | _ -> clr', rcs'
 
@@ -68,9 +68,8 @@ let pf_match = pf_apply (fun e s c t -> understand_tcc e s ~expected_type:t c)
 
 let apply_rconstr ?ist t gl =
 (* ppdebug(lazy(str"sigma@apply_rconstr=" ++ pr_evar_map None (project gl))); *)
-  let open CAst in
-  let n = match ist, t with
-    | None, { v = GVar id | GRef (VarRef id,_) } -> pf_nbargs gl (EConstr.mkVar id)
+  let n = match ist, DAst.get t with
+    | None, (GVar id | GRef (VarRef id,_)) -> pf_nbargs gl (EConstr.mkVar id)
     | Some ist, _ -> interp_nbargs ist gl t
     | _ -> anomaly "apply_rconstr without ist and not RVar" in
   let mkRlemma i = mkRApp t (mkRHoles i) in
diff --git a/plugins/ssr/ssrcommon.ml b/plugins/ssr/ssrcommon.ml
index 799e969ae..cf5fdf318 100644
--- a/plugins/ssr/ssrcommon.ml
+++ b/plugins/ssr/ssrcommon.ml
@@ -176,24 +176,26 @@ open Globnames
 open Misctypes
 open Decl_kinds
 
-let mkRHole = CAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
+let mkRHole = DAst.make @@ GHole (Evar_kinds.InternalHole, IntroAnonymous, None)
 
 let rec mkRHoles n = if n > 0 then mkRHole :: mkRHoles (n - 1) else []
-let rec isRHoles = function { CAst.v = GHole _ } :: cl -> isRHoles cl | cl -> cl = []
-let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
-let mkRVar id = CAst.make @@ GRef (VarRef id,None)
-let mkRltacVar id = CAst.make @@ GVar (id)
-let mkRCast rc rt =  CAst.make @@ GCast (rc, CastConv rt)
-let mkRType =  CAst.make @@ GSort (GType [])
-let mkRProp =  CAst.make @@ GSort (GProp)
-let mkRArrow rt1 rt2 = CAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
-let mkRConstruct c = CAst.make @@ GRef (ConstructRef c,None)
-let mkRInd mind = CAst.make @@ GRef (IndRef mind,None)
-let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
+let rec isRHoles cl = match cl with
+| [] -> true
+| c :: l -> match DAst.get c with GHole _ -> isRHoles l | _ -> false
+let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
+let mkRVar id = DAst.make @@ GRef (VarRef id,None)
+let mkRltacVar id = DAst.make @@ GVar (id)
+let mkRCast rc rt =  DAst.make @@ GCast (rc, CastConv rt)
+let mkRType =  DAst.make @@ GSort (GType [])
+let mkRProp =  DAst.make @@ GSort (GProp)
+let mkRArrow rt1 rt2 = DAst.make @@ GProd (Anonymous, Explicit, rt1, rt2)
+let mkRConstruct c = DAst.make @@ GRef (ConstructRef c,None)
+let mkRInd mind = DAst.make @@ GRef (IndRef mind,None)
+let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 let rec mkRnat n =
-  if n <= 0 then CAst.make @@ GRef (Coqlib.glob_O, None) else
-  mkRApp (CAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)]
+  if n <= 0 then DAst.make @@ GRef (Coqlib.glob_O, None) else
+  mkRApp (DAst.make @@ GRef (Coqlib.glob_S, None)) [mkRnat (n - 1)]
 
 let glob_constr ist genv = function
   | _, Some ce ->
@@ -710,7 +712,7 @@ let mkSsrRef name =
   try locate_reference (ssrqid name) with Not_found ->
   try locate_reference (ssrtopqid name) with Not_found ->
   CErrors.user_err (Pp.str "Small scale reflection library not loaded")
-let mkSsrRRef name = (CAst.make @@ GRef (mkSsrRef name,None)), None
+let mkSsrRRef name = (DAst.make @@ GRef (mkSsrRef name,None)), None
 let mkSsrConst name env sigma =
   EConstr.fresh_global env sigma (mkSsrRef name)
 let pf_mkSsrConst name gl =
@@ -845,10 +847,10 @@ let pf_interp_ty ?(resolve_typeclasses=false) ist gl ty =
    let n_binders = ref 0 in
    let ty = match ty with
    | a, (t, None) ->
-    let rec force_type ty = CAst.(map (function
+    let rec force_type ty = DAst.(map (function
      | GProd (x, k, s, t) -> incr n_binders; GProd (x, k, s, force_type t)
      | GLetIn (x, v, oty, t) -> incr n_binders; GLetIn (x, v, oty, force_type t)
-     | _ -> (mkRCast ty mkRType).v)) ty in
+     | _ -> DAst.get (mkRCast ty mkRType))) ty in
      a, (force_type t, None)
    | _, (_, Some ty) ->
     let rec force_type ty = CAst.(map (function
diff --git a/plugins/ssr/ssrequality.ml b/plugins/ssr/ssrequality.ml
index ab6a60f4e..8b69c3435 100644
--- a/plugins/ssr/ssrequality.ml
+++ b/plugins/ssr/ssrequality.ml
@@ -129,7 +129,7 @@ let newssrcongrtac arg ist gl =
     let eq, gl = pf_fresh_global (Coqlib.build_coq_eq ()) gl in
     pf_saturate gl (EConstr.of_constr eq) 3 in
   tclMATCH_GOAL (equality, gl') (fun gl' -> fs gl' (List.assoc 0 eq_args))
-  (fun ty -> congrtac (arg, Detyping.detype false [] (pf_env gl) (project gl) ty) ist)
+  (fun ty -> congrtac (arg, Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) ty) ist)
   (fun () ->
     let lhs, gl' = mk_evar gl EConstr.mkProp in let rhs, gl' = mk_evar gl' EConstr.mkProp in
     let arrow = EConstr.mkArrow lhs (EConstr.Vars.lift 1 rhs) in
diff --git a/plugins/ssr/ssrfwd.ml b/plugins/ssr/ssrfwd.ml
index 8e6329a15..d01bdc1b9 100644
--- a/plugins/ssr/ssrfwd.ml
+++ b/plugins/ssr/ssrfwd.ml
@@ -184,9 +184,13 @@ let havetac ist
       mkt ct, mkt cty, mkt (mkCHole None), loc
     | _, (_, Some ct) ->
       mkt ct, mkt (mkCHole None), mkt (mkCHole None), None
-    | _, ({ loc; v = GCast (ct, CastConv cty) }, None) ->
-      mkl ct, mkl cty, mkl mkRHole, loc
-    | _, (t, None) -> mkl t, mkl mkRHole, mkl mkRHole, None in
+    | _, (t, None) ->
+      begin match DAst.get t with
+      | GCast (ct, CastConv cty) ->
+        mkl ct, mkl cty, mkl mkRHole, t.CAst.loc
+      | _ -> mkl t, mkl mkRHole, mkl mkRHole, None
+      end
+  in
   let gl, cut, sol, itac1, itac2 =
    match fk, namefst, suff with
    | FwdHave, true, true ->
@@ -323,11 +327,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
   let mkpats = function
   | _, Some ((x, _), _) -> fun pats -> IPatId (hoi_id x) :: pats
   | _ -> fun x -> x in
-  let open CAst in
   let ct = match ct with
-  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
-  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
-  | _ -> anomaly "wlog: ssr cast hole deleted by typecheck" in
+  | (a, (b, Some ct)) ->
+    begin match ct.CAst.v with
+    | CCast (_, CastConv cty) -> a, (b, Some cty)
+    | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
+    end
+  | (a, (t, None)) ->
+    begin match DAst.get t with
+    | GCast (_, CastConv cty) -> a, (cty, None)
+    | _ -> anomaly "wlog: ssr cast hole deleted by typecheck"
+    end
+  in
   let cut_implies_goal = not (suff || ghave <> `NoGen) in
   let c, args, ct, gl =
     let gens = List.filter (function _, Some _ -> true | _ -> false) gens in
@@ -398,11 +409,18 @@ let wlogtac ist (((clr0, pats),_),_) (gens, ((_, ct))) hint suff ghave gl =
 
 let sufftac ist ((((clr, pats),binders),simpl), ((_, c), hint)) =
   let htac = Tacticals.tclTHEN (introstac ~ist pats) (hinttac ist true hint) in
-  let open CAst in
   let c = match c with
-  | (a, (b, Some { v = CCast (_, CastConv cty)})) -> a, (b, Some cty)
-  | (a, ({ v = GCast (_, CastConv cty) }, None)) -> a, (cty, None)
-  | _ -> anomaly "suff: ssr cast hole deleted by typecheck" in
+  | (a, (b, Some ct)) ->
+    begin match ct.CAst.v with
+    | CCast (_, CastConv cty) -> a, (b, Some cty)
+    | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
+    end
+  | (a, (t, None)) ->
+    begin match DAst.get t with
+    | GCast (_, CastConv cty) -> a, (cty, None)
+    | _ -> anomaly "suff: ssr cast hole deleted by typecheck"
+    end
+  in
   let ctac gl =
     let _,ty,_,uc = pf_interp_ty ist gl c in let gl = pf_merge_uc uc gl in
     basecuttac "ssr_suff" ty gl in
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index db1981228..060225dab 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -342,7 +342,7 @@ let interp_index ist gl idx =
         | None ->
         begin match Tacinterp.Value.to_constr v with
         | Some c ->
-          let rc = Detyping.detype false [] (pf_env gl) (project gl) c in
+          let rc = Detyping.detype Detyping.Now false [] (pf_env gl) (project gl) c in
           begin match Notation.uninterp_prim_token rc with
           | _, Constrexpr.Numeral (s,b) ->
              let n = int_of_string s in if b then n else -n
@@ -1062,32 +1062,32 @@ let rec format_glob_decl h0 d0 = match h0, d0 with
      Bdef (x, None, v) :: format_glob_decl [] d
   | _, [] -> []
 
-let rec format_glob_constr h0 c0 = let open CAst in match h0, c0 with
-  | BFvar :: h, { v = GLambda (x, _, _, c) } ->
+let rec format_glob_constr h0 c0 = match h0, DAst.get c0 with
+  | BFvar :: h, GLambda (x, _, _, c) ->
     let bs, c' = format_glob_constr h c in
     Bvar x :: bs, c'
-  | BFdecl 1 :: h, { v = GLambda (x, _, t, c) } ->
+  | BFdecl 1 :: h, GLambda (x, _, t, c) ->
     let bs, c' = format_glob_constr h c in
     Bdecl ([x], t) :: bs, c'
-  | BFdecl n :: h, { v = GLambda (x, _, t, c) } when n > 1 ->
+  | BFdecl n :: h, GLambda (x, _, t, c) when n > 1 ->
     begin match format_glob_constr (BFdecl (n - 1) :: h) c with
     | Bdecl (xs, _) :: bs, c' -> Bdecl (x :: xs, t) :: bs, c'
     | _ -> [Bdecl ([x], t)], c
     end
-  | BFdef :: h, { v = GLetIn(x, v, oty, c) } ->
+  | BFdef :: h, GLetIn(x, v, oty, c) ->
     let bs, c' = format_glob_constr h c in
     Bdef (x, oty, v) :: bs, c'
-  | [BFcast], { v = GCast (c, CastConv t) } ->
+  | [BFcast], GCast (c, CastConv t) ->
     [Bcast t], c
-  | BFrec (has_str, has_cast) :: h, { v = GRec (f, _, bl, t, c) }
+  | BFrec (has_str, has_cast) :: h, GRec (f, _, bl, t, c)
       when Array.length c = 1 ->
     let bs = format_glob_decl h bl.(0) in
     let bstr = match has_str, f with
     | true, GFix ([|Some i, GStructRec|], _) -> mkBstruct i bs
     | _ -> [] in
     bs @ bstr @ (if has_cast then [Bcast t.(0)] else []), c.(0)
-  | _, c ->
-    [], c
+  | _, _ ->
+    [], c0
 
 (** Forward chaining argument *)
 
diff --git a/plugins/ssr/ssrvernac.ml4 b/plugins/ssr/ssrvernac.ml4
index 9c59d83d4..507b4631b 100644
--- a/plugins/ssr/ssrvernac.ml4
+++ b/plugins/ssr/ssrvernac.ml4
@@ -292,7 +292,7 @@ let interp_search_notation ?loc tag okey =
     err (pr_ntn ntn ++ str " is an n-ary notation");
   let nvars = List.filter (fun (_,(_,typ)) -> typ = NtnTypeConstr) nvars in
   let rec sub () = function
-  | NVar x when List.mem_assoc x nvars -> CAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
+  | NVar x when List.mem_assoc x nvars -> DAst.make ?loc @@ GPatVar (FirstOrderPatVar x)
   | c ->
     glob_constr_of_notation_constr_with_binders ?loc (fun _ x -> (), x) sub () c in
   let _, npat = Patternops.pattern_of_glob_constr (sub () body) in
@@ -467,10 +467,10 @@ let pr_raw_ssrhintref prc _ _ = let open CAst in function
     prc c ++ str "|" ++ int (List.length args)
   | c -> prc c
 
-let pr_rawhintref = let open CAst in function
-  | { v = GApp (f, args) } when isRHoles args ->
+let pr_rawhintref c = match DAst.get c with
+  | GApp (f, args) when isRHoles args ->
     pr_glob_constr f ++ str "|" ++ int (List.length args)
-  | c -> pr_glob_constr c
+  | _ -> pr_glob_constr c
 
 let pr_glob_ssrhintref _ _ _ (c, _) = pr_rawhintref c
 
diff --git a/plugins/ssr/ssrview.ml b/plugins/ssr/ssrview.ml
index 338ecccc2..61b65e347 100644
--- a/plugins/ssr/ssrview.ml
+++ b/plugins/ssr/ssrview.ml
@@ -59,13 +59,13 @@ let glob_view_hints lvh =
 
 let add_view_hints lvh i = Lib.add_anonymous_leaf (in_viewhint (i, lvh))
 
-let interp_view ist si env sigma gv v rid =
-  let open CAst in
-  match v with
-  | { v = GApp ( { v = GHole _ } , rargs); loc } ->
-    let rv = make ?loc @@ GApp (rid, rargs) in
+let interp_view ist si env sigma gv rv rid =
+  match DAst.get rv with
+  | GApp (h, rargs) when (match DAst.get h with GHole _ -> true | _ -> false) ->
+    let loc = rv.CAst.loc in
+    let rv = DAst.make ?loc @@ GApp (rid, rargs) in
     snd (interp_open_constr ist (re_sig si sigma) (rv, None))
-  | rv ->
+  | _ ->
   let interp rc rargs =
     interp_open_constr ist (re_sig si sigma) (mkRApp rc rargs, None) in
   let rec simple_view rargs n =
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index f6300ab7e..2e5522b83 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -134,6 +134,10 @@ let dC t = CastConv t
 let isCVar   = function { CAst.v = CRef (Ident _, _) } -> true | _ -> false
 let destCVar = function { CAst.v = CRef (Ident (_, id), _) } -> id | _ ->
   CErrors.anomaly (str"not a CRef.")
+let isGLambda c = match DAst.get c with GLambda (Name _, _, _, _) -> true | _ -> false
+let destGLambda c = match DAst.get c with GLambda (Name id, _, _, c) -> (id, c)
+  | _ -> CErrors.anomaly (str "not a GLambda")
+let isGHole c = match DAst.get c with GHole _ -> true | _ -> false
 let mkCHole ~loc = CAst.make ?loc @@ CHole (None, IntroAnonymous, None)
 let mkCLambda ?loc name ty t = CAst.make ?loc @@
    CLambdaN ([[Loc.tag ?loc name], Default Explicit, ty], t)
@@ -141,10 +145,10 @@ let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((Loc.tag ?loc name), bo, None, t)
 let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
-let mkRHole = CAst.make @@ GHole (InternalHole, IntroAnonymous, None)
-let mkRApp f args = if args = [] then f else CAst.make @@ GApp (f, args)
-let mkRCast rc rt =  CAst.make @@ GCast (rc, dC rt)
-let mkRLambda n s t = CAst.make @@ GLambda (n, Explicit, s, t)
+let mkRHole = DAst.make @@ GHole (InternalHole, IntroAnonymous, None)
+let mkRApp f args = if args = [] then f else DAst.make @@ GApp (f, args)
+let mkRCast rc rt =  DAst.make @@ GCast (rc, dC rt)
+let mkRLambda n s t = DAst.make @@ GLambda (n, Explicit, s, t)
 
 (* ssrterm conbinators *)
 let combineCG t1 t2 f g = match t1, t2 with
@@ -980,11 +984,10 @@ let pr_rpattern = pr_pattern
 
 type pattern = Evd.evar_map * (constr, constr) ssrpattern
 
-
-let id_of_cpattern = let open CAst in function
-  | _,(_,Some { v = CRef (Ident (_, x), _) } ) -> Some x
-  | _,(_,Some { v = CAppExpl ((_, Ident (_, x), _), []) } ) -> Some x
-  | _,({ v = GRef (VarRef x, _)} ,None) -> Some x
+let id_of_cpattern (_, (c1, c2)) = let open CAst in match DAst.get c1, c2 with
+  | _, Some { v = CRef (Ident (_, x), _) } -> Some x
+  | _, Some { v = CAppExpl ((_, Ident (_, x), _), []) } -> Some x
+  | GRef (VarRef x, _), None -> Some x
   | _ -> None
 let id_of_Cterm t = match id_of_cpattern t with
   | Some x -> x
@@ -1082,10 +1085,11 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   let eAsXInT e x t = E_As_X_In_T(e,x,t) in
   let mkG ?(k=' ') x = k,(x,None) in
   let decode ist t ?reccall f g =
-    let open CAst in
-    try match (pf_intern_term ist gl t) with
-    | { v = GCast({ v = GHole _},CastConv({ v = GLambda(Name x,_,_,c)})) } -> f x (' ',(c,None))
-    | { v = GVar id }
+    try match DAst.get (pf_intern_term ist gl t) with
+    | GCast(t,CastConv c) when isGHole t && isGLambda c->
+      let (x, c) = destGLambda c in
+      f x (' ',(c,None))
+    | GVar id
       when Id.Map.mem id ist.lfun &&
            not(Option.is_empty reccall) &&
            not(Option.is_empty wit_ssrpatternarg) ->
@@ -1126,19 +1130,27 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
         thin name sigma e)
       sigma new_evars in
     sigma in
-  let red = let rec decode_red (ist,red) = let open CAst in match red with
-    | T(k,({ v = GCast ({ v = GHole _ },CastConv({ v = GLambda (Name id,_,_,t)}))},None))
-        when let id = Id.to_string id in let len = String.length id in
+  let red = let rec decode_red (ist,red) = match red with
+    | T(k,(t,None)) ->
+      begin match DAst.get t with
+      | GCast (c,CastConv t)
+        when isGHole c &&
+          let (id, t) = destGLambda t in
+          let id = Id.to_string id in let len = String.length id in
         (len > 8 && String.sub id 0 8 = "_ssrpat_") ->
+        let (id, t) = destGLambda t in
         let id = Id.to_string id in let len = String.length id in
-        (match String.sub id 8 (len - 8), t with
-        | "In", { v = GApp( _, [t]) } -> decodeG t xInT (fun x -> T x)
-        | "In", { v = GApp( _, [e; t]) } -> decodeG t (eInXInT (mkG e)) (bad_enc id)
-        | "In", { v = GApp( _, [e; t; e_in_t]) } ->
+        (match String.sub id 8 (len - 8), DAst.get t with
+        | "In", GApp( _, [t]) -> decodeG t xInT (fun x -> T x)
+        | "In", GApp( _, [e; t]) -> decodeG t (eInXInT (mkG e)) (bad_enc id)
+        | "In", GApp( _, [e; t; e_in_t]) ->
             decodeG t (eInXInT (mkG e))
               (fun _ -> decodeG e_in_t xInT (fun _ -> assert false))
-        | "As", { v = GApp(_, [e; t]) } -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
+        | "As", GApp(_, [e; t]) -> decodeG t (eAsXInT (mkG e)) (bad_enc id)
         | _ -> bad_enc id ())
+      | _ ->
+        decode ist ~reccall:decode_red (k, (t, None)) xInT (fun x -> T x)
+      end
     | T t -> decode ist ~reccall:decode_red t xInT (fun x -> T x)
     | In_T t -> decode ist t inXInT inT
     | X_In_T (e,t) -> decode ist t (eInXInT e) (fun x -> xInT (id_of_Cterm e) x)
@@ -1163,7 +1175,7 @@ let interp_pattern ?wit_ssrpatternarg ist gl red redty =
   pp(lazy(str"typed as: " ++ pr_pattern_w_ids red));
   let mkXLetIn ?loc x (a,(g,c)) = match c with
   | Some b -> a,(g,Some (mkCLetIn ?loc x (mkCHole ~loc) b))
-  | None -> a,(CAst.make ?loc @@ GLetIn (x, CAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
+  | None -> a,(DAst.make ?loc @@ GLetIn (x, DAst.make ?loc @@ GHole (BinderType x, IntroAnonymous, None), None, g), None) in
   match red with
   | T t -> let sigma, t = interp_term ist gl t in sigma, T t
   | In_T t -> let sigma, t = interp_term ist gl t in sigma, In_T t
@@ -1336,10 +1348,10 @@ let pf_fill_occ_term gl occ t =
   let cl,(_,t) = fill_occ_term env concl occ sigma0 t in
   cl, t
 
-let cpattern_of_id id = ' ', (CAst.make @@ GRef (VarRef  id, None), None)
+let cpattern_of_id id = ' ', (DAst.make @@ GRef (VarRef  id, None), None)
 
-let is_wildcard : cpattern -> bool = function
-  | _,(_,Some { CAst.v = CHole _ } | { CAst.v = GHole _ } ,None) -> true
+let is_wildcard ((_, (l, r)) : cpattern) : bool = match DAst.get l, r with
+  | _, Some { CAst.v = CHole _ } | GHole _, None -> true
   | _ -> false
 
 (* "ssrpattern" *)
diff --git a/plugins/syntax/ascii_syntax.ml b/plugins/syntax/ascii_syntax.ml
index c41ec39cb..b299ff853 100644
--- a/plugins/syntax/ascii_syntax.ml
+++ b/plugins/syntax/ascii_syntax.ml
@@ -25,6 +25,10 @@ let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_kn dir id = Globnames.encode_mind (make_dir dir) (Id.of_string id)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let ascii_module = ["Coq";"Strings";"Ascii"]
 
 let ascii_path = make_path ascii_module "ascii"
@@ -42,9 +46,9 @@ let interp_ascii ?loc p =
   let rec aux n p =
      if Int.equal n 0 then [] else
      let mp = p mod 2 in
-     (CAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
+     (DAst.make ?loc @@ GRef ((if Int.equal mp 0 then glob_false else glob_true),None))
      :: (aux (n-1) (p/2)) in
-  CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
+  DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef(force glob_Ascii,None), aux 8 p)
 
 let interp_ascii_string ?loc s =
   let p =
@@ -60,12 +64,12 @@ let interp_ascii_string ?loc s =
 let uninterp_ascii r =
   let rec uninterp_bool_list n = function
     | [] when Int.equal n 0 -> 0
-    | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
-    | { CAst.v = GRef (k,_)}::l when Globnames.eq_gr k glob_false -> 2*(uninterp_bool_list (n-1) l)
+    | r::l when is_gr r glob_true  -> 1+2*(uninterp_bool_list (n-1)  l)
+    | r::l when is_gr r glob_false -> 2*(uninterp_bool_list (n-1) l)
     | _ -> raise Non_closed_ascii in
   try
-    let aux = function
-    | { CAst.v = GApp ({ CAst.v = GRef (k,_)},l) } when Globnames.eq_gr k (force glob_Ascii) -> uninterp_bool_list 8 l
+    let aux c = match DAst.get c with
+    | GApp (r, l) when is_gr r (force glob_Ascii) -> uninterp_bool_list 8 l
     | _ -> raise Non_closed_ascii in
     Some (aux r)
   with
@@ -75,10 +79,10 @@ let make_ascii_string n =
   if n>=32 && n<=126 then String.make 1 (char_of_int n)
   else Printf.sprintf "%03d" n
 
-let uninterp_ascii_string r = Option.map make_ascii_string (uninterp_ascii r)
+let uninterp_ascii_string (AnyGlobConstr r) = Option.map make_ascii_string (uninterp_ascii r)
 
 let _ =
   Notation.declare_string_interpreter "char_scope"
     (ascii_path,ascii_module)
     interp_ascii_string
-    ([CAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
+    ([DAst.make @@ GRef (static_glob_Ascii,None)], uninterp_ascii_string, true)
diff --git a/plugins/syntax/int31_syntax.ml b/plugins/syntax/int31_syntax.ml
index af64b1479..0dff047a3 100644
--- a/plugins/syntax/int31_syntax.ml
+++ b/plugins/syntax/int31_syntax.ml
@@ -23,6 +23,10 @@ open Glob_term
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let make_mind mp id = Names.MutInd.make2 mp (Label.make id)
 let make_mind_mpfile dir id = make_mind (ModPath.MPfile (make_dir dir)) id
 let make_mind_mpdot dir modname id =
@@ -49,9 +53,9 @@ exception Non_closed
 (* parses a *non-negative* integer (from bigint.ml) into an int31
    wraps modulo 2^31 *)
 let int31_of_pos_bigint ?loc n =
-  let ref_construct = CAst.make ?loc (GRef (int31_construct, None)) in
-  let ref_0 = CAst.make ?loc (GRef (int31_0, None)) in
-  let ref_1 = CAst.make ?loc (GRef (int31_1, None)) in
+  let ref_construct = DAst.make ?loc (GRef (int31_construct, None)) in
+  let ref_0 = DAst.make ?loc (GRef (int31_0, None)) in
+  let ref_1 = DAst.make ?loc (GRef (int31_1, None)) in
   let rec args counter n =
     if counter <= 0 then
       []
@@ -59,7 +63,7 @@ let int31_of_pos_bigint ?loc n =
       let (q,r) = div2_with_rest n in
 	(if r then ref_1 else ref_0)::(args (counter-1) q)
   in
-  CAst.make ?loc (GApp (ref_construct, List.rev (args 31 n)))
+  DAst.make ?loc (GApp (ref_construct, List.rev (args 31 n)))
 
 let error_negative ?loc =
   CErrors.user_err ?loc ~hdr:"interp_int31" (Pp.str "int31 are only non-negative numbers.")
@@ -76,15 +80,15 @@ let bigint_of_int31 =
   let rec args_parsing args cur =
     match args with
       | [] -> cur
-      | { CAst.v = GRef (b,_) }::l when eq_gr b int31_0 -> args_parsing l (mult_2 cur)
-      | { CAst.v = GRef (b,_) }::l when eq_gr b int31_1 -> args_parsing l (add_1 (mult_2 cur))
+      | r::l when is_gr r int31_0 -> args_parsing l (mult_2 cur)
+      | r::l when is_gr r int31_1 -> args_parsing l (add_1 (mult_2 cur))
       | _ -> raise Non_closed
   in
-  function
-  | { CAst.v = GApp ({ CAst.v = GRef (c, _) }, args) } when eq_gr c int31_construct -> args_parsing args zero
+  fun c -> match DAst.get c with
+  | GApp (r, args) when is_gr r int31_construct -> args_parsing args zero
   | _ -> raise Non_closed
 
-let uninterp_int31 i =
+let uninterp_int31 (AnyGlobConstr i) =
   try
     Some (bigint_of_int31 i)
   with Non_closed ->
@@ -94,6 +98,6 @@ let uninterp_int31 i =
 let _ = Notation.declare_numeral_interpreter int31_scope
   (int31_path, int31_module)
   interp_int31
-  ([CAst.make (GRef (int31_construct, None))],
+  ([DAst.make (GRef (int31_construct, None))],
    uninterp_int31,
    true)
diff --git a/plugins/syntax/nat_syntax.ml b/plugins/syntax/nat_syntax.ml
index 524a5c522..2f9870cf9 100644
--- a/plugins/syntax/nat_syntax.ml
+++ b/plugins/syntax/nat_syntax.ml
@@ -37,11 +37,11 @@ let warn_large_nat =
 let nat_of_int ?loc n =
   if is_pos_or_zero n then begin
       if less_than threshold n then warn_large_nat ();
-      let ref_O = CAst.make ?loc @@ GRef (glob_O, None) in
-      let ref_S = CAst.make ?loc @@ GRef (glob_S, None) in
+      let ref_O = DAst.make ?loc @@ GRef (glob_O, None) in
+      let ref_S = DAst.make ?loc @@ GRef (glob_S, None) in
       let rec mk_nat acc n =
 	if n <> zero then
-	  mk_nat (CAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
+	  mk_nat (DAst.make ?loc @@ GApp (ref_S, [acc])) (sub_1 n)
 	else
 	  acc
       in
@@ -56,13 +56,17 @@ let nat_of_int ?loc n =
 
 exception Non_closed_number
 
-let rec int_of_nat x = CAst.with_val (function
-  | GApp ({ CAst.v = GRef (s,_) } ,[a]) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+let rec int_of_nat x = DAst.with_val (function
+  | GApp (r, [a]) ->
+    begin match DAst.get r with
+    | GRef (s,_) when Globnames.eq_gr s glob_S -> add_1 (int_of_nat a)
+    | _ -> raise Non_closed_number
+    end
   | GRef (z,_) when Globnames.eq_gr z glob_O -> zero
   | _ -> raise Non_closed_number
   ) x
 
-let uninterp_nat p =
+let uninterp_nat (AnyGlobConstr p) =
   try
     Some (int_of_nat p)
   with
@@ -75,4 +79,4 @@ let _ =
   Notation.declare_numeral_interpreter "nat_scope"
     (nat_path,datatypes_module_name)
     nat_of_int
-    ([CAst.make @@ GRef (glob_S,None); CAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
+    ([DAst.make @@ GRef (glob_S,None); DAst.make @@ GRef (glob_O,None)], uninterp_nat, true)
diff --git a/plugins/syntax/r_syntax.ml b/plugins/syntax/r_syntax.ml
index 06117de79..88ff38c6d 100644
--- a/plugins/syntax/r_syntax.ml
+++ b/plugins/syntax/r_syntax.ml
@@ -27,6 +27,10 @@ let binnums = ["Coq";"Numbers";"BinNums"]
 let make_dir l = DirPath.make (List.rev_map Id.of_string l)
 let make_path dir id = Libnames.make_path (make_dir dir) (Id.of_string id)
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 let positive_path = make_path binnums "positive"
 
 (* TODO: temporary hack *)
@@ -42,13 +46,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x =
-  let ref_xI = CAst.make @@ GRef (glob_xI, None) in
-  let ref_xH = CAst.make @@ GRef (glob_xH, None) in
-  let ref_xO = CAst.make @@ GRef (glob_xO, None) in
+  let ref_xI = DAst.make @@ GRef (glob_xI, None) in
+  let ref_xH = DAst.make @@ GRef (glob_xH, None) in
+  let ref_xO = DAst.make @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> CAst.make @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> CAst.make @@ GApp (ref_xI,[pos_of q])
+      | (q,false) -> DAst.make @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> DAst.make @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -57,10 +61,10 @@ let pos_of_bignat ?loc x =
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
 
-let rec bignat_of_pos = function
-  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
-  | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_xH -> Bigint.one
+let rec bignat_of_pos c = match DAst.get c with
+  | GApp (r, [a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (r, [a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
+  | GRef (a, _) when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -81,18 +85,18 @@ let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    CAst.make @@ GApp(CAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
+    DAst.make @@ GApp(DAst.make @@ GRef (sgn,None), [pos_of_bignat ?loc n])
   else
-    CAst.make @@ GRef (glob_ZERO, None)
+    DAst.make @@ GRef (glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_z = function
-  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | { CAst.v = GApp ({ CAst.v = GRef (b,_)},[a]) } when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
-  | { CAst.v = GRef (a, _) } when Globnames.eq_gr a glob_ZERO -> Bigint.zero
+let bigint_of_z c = match DAst.get c with
+  | GApp (r,[a]) when is_gr r glob_POS -> bignat_of_pos a
+  | GApp (r,[a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
+  | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
 
 (**********************************************************************)
@@ -108,18 +112,18 @@ let make_path dir id = Globnames.encode_con dir (Id.of_string id)
 let glob_IZR = ConstRef (make_path (make_dir rdefinitions) "IZR")
 
 let r_of_int ?loc z =
-  CAst.make @@ GApp (CAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
+  DAst.make @@ GApp (DAst.make @@ GRef(glob_IZR,None), [z_of_int ?loc z])
 
 (**********************************************************************)
 (* Printing R via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_r = function
-  | { CAst.v = GApp ({ CAst.v = GRef (o,_) }, [a]) } when Globnames.eq_gr o glob_IZR ->
+let bigint_of_r c = match DAst.get c with
+  | GApp (r, [a]) when is_gr r glob_IZR ->
       bigint_of_z a
   | _ -> raise Non_closed_number
 
-let uninterp_r p =
+let uninterp_r (AnyGlobConstr p) =
   try
     Some (bigint_of_r p)
   with Non_closed_number ->
@@ -128,6 +132,6 @@ let uninterp_r p =
 let _ = Notation.declare_numeral_interpreter "R_scope"
   (r_path,["Coq";"Reals";"Rdefinitions"])
   r_of_int
-  ([CAst.make @@ GRef (glob_IZR, None)],
+  ([DAst.make @@ GRef (glob_IZR, None)],
     uninterp_r,
     false)
diff --git a/plugins/syntax/string_syntax.ml b/plugins/syntax/string_syntax.ml
index b7f13b040..cc82fc94c 100644
--- a/plugins/syntax/string_syntax.ml
+++ b/plugins/syntax/string_syntax.ml
@@ -31,25 +31,29 @@ let make_reference id = find_reference "String interpretation" string_module id
 let glob_String = lazy (make_reference "String")
 let glob_EmptyString = lazy (make_reference "EmptyString")
 
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
 open Lazy
 
 let interp_string ?loc s =
   let le = String.length s in
   let rec aux n =
-     if n = le then CAst.make ?loc @@ GRef (force glob_EmptyString, None) else
-     CAst.make ?loc @@ GApp (CAst.make ?loc @@ GRef (force glob_String, None),
+     if n = le then DAst.make ?loc @@ GRef (force glob_EmptyString, None) else
+     DAst.make ?loc @@ GApp (DAst.make ?loc @@ GRef (force glob_String, None),
        [interp_ascii ?loc (int_of_char s.[n]); aux (n+1)])
   in aux 0
 
-let uninterp_string r =
+let uninterp_string (AnyGlobConstr r) =
   try
     let b = Buffer.create 16 in
-    let rec aux = function
-    | { CAst.v = GApp ({ CAst.v = GRef (k,_) },[a;s]) } when eq_gr k (force glob_String) ->
+    let rec aux c = match DAst.get c with
+    | GApp (k,[a;s]) when is_gr k (force glob_String) ->
 	(match uninterp_ascii a with
 	  | Some c -> Buffer.add_char b (Char.chr c); aux s
 	  | _ -> raise Non_closed_string)
-    | { CAst.v = GRef (z,_) } when eq_gr z (force glob_EmptyString) ->
+    | GRef (z,_) when eq_gr z (force glob_EmptyString) ->
 	Some (Buffer.contents b)
     | _ ->
 	raise Non_closed_string
@@ -61,6 +65,6 @@ let _ =
   Notation.declare_string_interpreter "string_scope"
     (string_path,["Coq";"Strings";"String"])
     interp_string
-    ([CAst.make @@ GRef (static_glob_String,None);
-      CAst.make @@ GRef (static_glob_EmptyString,None)],
+    ([DAst.make @@ GRef (static_glob_String,None);
+      DAst.make @@ GRef (static_glob_EmptyString,None)],
      uninterp_string, true)
diff --git a/plugins/syntax/z_syntax.ml b/plugins/syntax/z_syntax.ml
index af3df2889..0d743a2b5 100644
--- a/plugins/syntax/z_syntax.ml
+++ b/plugins/syntax/z_syntax.ml
@@ -45,13 +45,13 @@ let glob_xO = ConstructRef path_of_xO
 let glob_xH = ConstructRef path_of_xH
 
 let pos_of_bignat ?loc x = 
-  let ref_xI = CAst.make ?loc @@ GRef (glob_xI, None) in
-  let ref_xH = CAst.make ?loc @@ GRef (glob_xH, None) in
-  let ref_xO = CAst.make ?loc @@ GRef (glob_xO, None) in
+  let ref_xI = DAst.make ?loc @@ GRef (glob_xI, None) in
+  let ref_xH = DAst.make ?loc @@ GRef (glob_xH, None) in
+  let ref_xO = DAst.make ?loc @@ GRef (glob_xO, None) in
   let rec pos_of x =
     match div2_with_rest x with
-      | (q,false) -> CAst.make ?loc @@ GApp (ref_xO,[pos_of q])
-      | (q,true) when not (Bigint.equal q zero) -> CAst.make ?loc @@ GApp (ref_xI,[pos_of q])
+      | (q,false) -> DAst.make ?loc @@ GApp (ref_xO,[pos_of q])
+      | (q,true) when not (Bigint.equal q zero) -> DAst.make ?loc @@ GApp (ref_xI,[pos_of q])
       | (q,true) -> ref_xH
   in
   pos_of x
@@ -68,14 +68,18 @@ let interp_positive ?loc n =
 (* Printing positive via scopes                                       *)
 (**********************************************************************)
 
-let rec bignat_of_pos x = CAst.with_val (function
-  | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xO -> mult_2(bignat_of_pos a)
-  | GApp ({ CAst.v = GRef (b,_) },[a]) when Globnames.eq_gr b glob_xI -> add_1(mult_2(bignat_of_pos a))
+let is_gr c gr = match DAst.get c with
+| GRef (r, _) -> Globnames.eq_gr r gr
+| _ -> false
+
+let rec bignat_of_pos x = DAst.with_val (function
+  | GApp (r ,[a]) when is_gr r glob_xO -> mult_2(bignat_of_pos a)
+  | GApp (r ,[a]) when is_gr r glob_xI -> add_1(mult_2(bignat_of_pos a))
   | GRef (a, _)                when Globnames.eq_gr a glob_xH -> Bigint.one
   | _ -> raise Non_closed_number
   ) x
 
-let uninterp_positive p =
+let uninterp_positive (AnyGlobConstr p) =
   try
     Some (bignat_of_pos p)
   with Non_closed_number ->
@@ -88,9 +92,9 @@ let uninterp_positive p =
 let _ = Notation.declare_numeral_interpreter "positive_scope"
   (positive_path,binnums)
   interp_positive
-  ([CAst.make @@ GRef (glob_xI, None);
-    CAst.make @@ GRef (glob_xO, None);
-    CAst.make @@ GRef (glob_xH, None)],
+  ([DAst.make @@ GRef (glob_xI, None);
+    DAst.make @@ GRef (glob_xO, None);
+    DAst.make @@ GRef (glob_xH, None)],
    uninterp_positive,
    true)
 
@@ -107,9 +111,9 @@ let glob_Npos = ConstructRef path_of_Npos
 
 let n_path = make_path binnums "N"
 
-let n_of_binnat ?loc pos_or_neg n = CAst.make ?loc @@
+let n_of_binnat ?loc pos_or_neg n = DAst.make ?loc @@
   if not (Bigint.equal n zero) then
-    GApp(CAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
+    GApp(DAst.make @@ GRef (glob_Npos,None), [pos_of_bignat ?loc n])
   else
     GRef(glob_N0, None)
 
@@ -124,13 +128,13 @@ let n_of_int ?loc n =
 (* Printing N via scopes                                              *)
 (**********************************************************************)
 
-let bignat_of_n = CAst.with_val (function
-  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_Npos -> bignat_of_pos a
+let bignat_of_n n = DAst.with_val (function
+  | GApp (r, [a]) when is_gr r glob_Npos -> bignat_of_pos a
   | GRef (a,_) when Globnames.eq_gr a glob_N0 -> Bigint.zero
   | _ -> raise Non_closed_number
-  )
+  ) n
 
-let uninterp_n p =
+let uninterp_n (AnyGlobConstr p) =
   try Some (bignat_of_n p)
   with Non_closed_number -> None
 
@@ -140,8 +144,8 @@ let uninterp_n p =
 let _ = Notation.declare_numeral_interpreter "N_scope"
   (n_path,binnums)
   n_of_int
-  ([CAst.make @@ GRef (glob_N0, None);
-    CAst.make @@ GRef (glob_Npos, None)],
+  ([DAst.make @@ GRef (glob_N0, None);
+    DAst.make @@ GRef (glob_Npos, None)],
   uninterp_n,
   true)
 
@@ -163,22 +167,22 @@ let z_of_int ?loc n =
   if not (Bigint.equal n zero) then
     let sgn, n =
       if is_pos_or_zero n then glob_POS, n else glob_NEG, Bigint.neg n in
-    CAst.make ?loc @@ GApp(CAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
+    DAst.make ?loc @@ GApp(DAst.make ?loc @@ GRef(sgn,None), [pos_of_bignat ?loc n])
   else
-    CAst.make ?loc @@ GRef(glob_ZERO, None)
+    DAst.make ?loc @@ GRef(glob_ZERO, None)
 
 (**********************************************************************)
 (* Printing Z via scopes                                              *)
 (**********************************************************************)
 
-let bigint_of_z = CAst.with_val (function
-  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_POS -> bignat_of_pos a
-  | GApp ({ CAst.v = GRef (b,_)},[a]) when Globnames.eq_gr b glob_NEG -> Bigint.neg (bignat_of_pos a)
+let bigint_of_z z = DAst.with_val (function
+  | GApp (r, [a]) when is_gr r glob_POS -> bignat_of_pos a
+  | GApp (r, [a]) when is_gr r glob_NEG -> Bigint.neg (bignat_of_pos a)
   | GRef (a, _) when Globnames.eq_gr a glob_ZERO -> Bigint.zero
   | _ -> raise Non_closed_number
-  )
+  ) z
 
-let uninterp_z p =
+let uninterp_z (AnyGlobConstr p) =
   try
     Some (bigint_of_z p)
   with Non_closed_number -> None
@@ -189,8 +193,8 @@ let uninterp_z p =
 let _ = Notation.declare_numeral_interpreter "Z_scope"
   (z_path,binnums)
   z_of_int
-  ([CAst.make @@ GRef (glob_ZERO, None);
-    CAst.make @@ GRef (glob_POS, None);
-    CAst.make @@ GRef (glob_NEG, None)],
+  ([DAst.make @@ GRef (glob_ZERO, None);
+    DAst.make @@ GRef (glob_POS, None);
+    DAst.make @@ GRef (glob_NEG, None)],
   uninterp_z,
   true)