[location] [ast] Switch Constrexpr AST to an extensible node type.

Following @gasche idea, and the original intention of #402, we switch
the main parsing AST of Coq from `'a Loc.located` to `'a CAst.ast`
which is private and record-based.

This provides significantly clearer code for the AST, and is robust
wrt attributes.

10 files changed, 60 insertions, 59 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 48ab3dd57c..938fe52373 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1246,15 +1246,16 @@ let compute_params_name relnames (args : (Name.t * Glob_term.glob_constr * glob_
   in
   List.rev !l
 
-let rec rebuild_return_type (loc, rt) =
-  match rt with
+let rec rebuild_return_type rt =
+  let loc = rt.CAst.loc in
+  match rt.CAst.v with
     | Constrexpr.CProdN(n,t') ->
-        Loc.tag ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
+        CAst.make ?loc @@ Constrexpr.CProdN(n,rebuild_return_type t')
     | Constrexpr.CLetIn(na,v,t,t') ->
-	Loc.tag ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
-    | _ -> Loc.tag ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
-				       Constrexpr.Default Decl_kinds.Explicit,Loc.tag ?loc rt],
-			    Loc.tag @@ Constrexpr.CSort(GType []))
+	CAst.make ?loc @@ Constrexpr.CLetIn(na,v,t,rebuild_return_type t')
+    | _ -> CAst.make ?loc @@ Constrexpr.CProdN([[Loc.tag Anonymous],
+				       Constrexpr.Default Decl_kinds.Explicit, rt],
+			    CAst.make @@ Constrexpr.CSort(GType []))
 
 let do_build_inductive
       evd (funconstants: Term.pconstant list) (funsargs: (Name.t * glob_constr * glob_constr option) list list)
@@ -1305,11 +1306,11 @@ let do_build_inductive
 	(fun (n,t,typ) acc ->
           match typ with
           | Some typ ->
-	     Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	     CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			      acc)
 	  | None ->
-	     Loc.tag @@ Constrexpr.CProdN
+	     CAst.make @@ Constrexpr.CProdN
 	       ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 		acc
 	       )
@@ -1372,11 +1373,11 @@ let do_build_inductive
       (fun (n,t,typ) acc ->
          match typ with
          | Some typ ->
-	   Loc.tag @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
+	   CAst.make @@ Constrexpr.CLetIn((Loc.tag n),with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t,
                               Some (with_full_print (Constrextern.extern_glob_constr Id.Set.empty) typ),
 			    acc)
 	 | None ->
-           Loc.tag @@ Constrexpr.CProdN
+           CAst.make @@ Constrexpr.CProdN
 	   ([[(Loc.tag n)],Constrexpr_ops.default_binder_kind,with_full_print (Constrextern.extern_glob_constr Id.Set.empty) t],
 	    acc
 	   )
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 3dc16626ce..f4e9aa3720 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -469,7 +469,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
   in
   let unbounded_eq =
     let f_app_args =
-      Loc.tag @@ Constrexpr.CAppExpl(
+      CAst.make @@ Constrexpr.CAppExpl(
 	 (None,(Ident (Loc.tag fname)),None) ,
 	 (List.map
 	    (function
@@ -480,7 +480,7 @@ let register_wf ?(is_mes=false) fname rec_impls wf_rel_expr wf_arg using_lemmas
 	 )
 	)
     in
-    Loc.tag @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
+    CAst.make @@ Constrexpr.CApp ((None,Constrexpr_ops.mkRefC (Qualid (Loc.tag (qualid_of_string "Logic.eq")))),
 		    [(f_app_args,None);(body,None)])
   in
   let eq = Constrexpr_ops.mkCProdN args unbounded_eq in
@@ -588,12 +588,12 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	  | [], _ -> (List.rev aux,replace_vars_constr_expr assoc typ,assoc)
 	  | (Constrexpr.CLocalAssum(nal,bk,_))::bl',typ ->
 	     rebuild_nal (aux,assoc) bk bl' nal (List.length nal) typ
-	  | (Constrexpr.CLocalDef(na,_,_))::bl',(_loc, Constrexpr.CLetIn(_,nat,ty,typ')) ->
+	  | (Constrexpr.CLocalDef(na,_,_))::bl',{ CAst.v = Constrexpr.CLetIn(_,nat,ty,typ') } ->
 	    rebuild_bl ((Constrexpr.CLocalDef(na,replace_vars_constr_expr assoc nat,Option.map (replace_vars_constr_expr assoc) ty (* ??? *))::aux),assoc)
 	      bl' typ'
 	  | _ -> assert false
       and rebuild_nal (aux,assoc) bk bl' nal lnal typ = 
-	match nal, snd typ with 
+	match nal, typ.CAst.v with 
 	  | [], _ -> rebuild_bl (aux,assoc) bl' typ
 	  | _,CProdN([],typ) -> rebuild_nal (aux,assoc) bk bl' nal lnal typ
 	  | _,CProdN((nal',bk',nal't)::rest,typ') -> 
@@ -606,7 +606,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	      rebuild_bl ((assum :: aux), nassoc) bl' 
 		(if List.is_empty new_nal' && List.is_empty rest
 		 then typ'
-		 else Loc.tag @@ if List.is_empty new_nal'
+		 else CAst.make @@ if List.is_empty new_nal'
 		 then CProdN(rest,typ')
 		 else CProdN(((new_nal',bk',nal't)::rest),typ'))
 	    else 
@@ -614,7 +614,7 @@ let rec rebuild_bl (aux,assoc) bl typ =
 	      let nassoc = make_assoc assoc nal' captured_nal in
 	      let assum = CLocalAssum(captured_nal,bk,replace_vars_constr_expr assoc nal't) in
 	      rebuild_nal ((assum :: aux), nassoc)
-		bk bl' non_captured_nal (lnal - lnal') (Loc.tag @@ CProdN(rest,typ'))
+		bk bl' non_captured_nal (lnal - lnal') (CAst.make @@ CProdN(rest,typ'))
 	  | _ -> assert false
 
 let rebuild_bl (aux,assoc) bl typ = rebuild_bl (aux,assoc) bl typ
@@ -725,7 +725,7 @@ let do_generate_principle pconstants on_error register_built interactive_proof
   in
   ()
 
-let rec add_args id new_args = Loc.map (function
+let rec add_args id new_args = CAst.map (function
   | CRef (r,_) as b ->
       begin match r with
 	| Libnames.Ident(loc,fname) when Id.equal fname id ->
@@ -794,7 +794,7 @@ let rec chop_n_arrow n t =
   if n <= 0
   then t (* If we have already removed all the arrows then return the type *)
   else (* If not we check the form of [t] *)
-    match snd t with
+    match t.CAst.v with
       | Constrexpr.CProdN(nal_ta',t') -> (* If we have a forall, to result are possible :
 					     either we need to discard more than the number of arrows contained
 					     in this product declaration then we just recall [chop_n_arrow] on
@@ -813,7 +813,7 @@ let rec chop_n_arrow n t =
 		    then
 		      aux (n - nal_l) nal_ta'
 		    else
-		      let new_t' = Loc.tag @@
+		      let new_t' = CAst.make @@
 			Constrexpr.CProdN(
 					((snd (List.chop n nal)),k,t'')::nal_ta',t')
 		      in
@@ -829,7 +829,7 @@ let rec chop_n_arrow n t =
 
 let rec get_args b t : Constrexpr.local_binder_expr list *
     Constrexpr.constr_expr * Constrexpr.constr_expr =
-  match snd b with
+  match b.CAst.v with
     | Constrexpr.CLambdaN ((nal_ta), b') ->
 	begin
 	  let n =
@@ -869,7 +869,7 @@ let make_graph (f_ref:global_reference) =
 	 in
 	 let (nal_tas,b,t)  = get_args extern_body extern_type in
 	 let expr_list =
-	   match snd b with
+	   match b.CAst.v with
 	     | Constrexpr.CFix(l_id,fixexprl) ->
 		 let l =
 		   List.map
@@ -882,7 +882,7 @@ let make_graph (f_ref:global_reference) =
 				  | Constrexpr.CLocalDef (na,_,_)-> []
 				  | Constrexpr.CLocalAssum (nal,_,_) ->
 				      List.map
-					(fun (loc,n) -> Loc.tag ?loc @@ 
+					(fun (loc,n) -> CAst.make ?loc @@ 
 					   CRef(Libnames.Ident(loc, Nameops.out_name n),None))
 					nal
                                   | Constrexpr.CLocalPattern _ -> assert false
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index f2654b5de8..5b51a213a1 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -73,7 +73,7 @@ let isVarf f x =
     in global environment. *)
 let ident_global_exist id =
   try
-    let ans = Loc.tag @@ CRef (Libnames.Ident (Loc.tag id), None) in
+    let ans = CAst.make @@ CRef (Libnames.Ident (Loc.tag id), None) in
     let _ = ignore (Constrintern.intern_constr (Global.env()) ans) in
     true
   with e when CErrors.noncritical e -> false
@@ -835,7 +835,7 @@ let merge_rec_params_and_arity prms1 prms2 shift (concl:constr) =
         let c = RelDecl.get_type decl in
         let typ = Constrextern.extern_constr false env Evd.empty c in
         let newenv = Environ.push_rel (LocalAssum (nm,c)) env in
-        Loc.tag @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
+        CAst.make @@ CProdN ([[(Loc.tag nm)],Constrexpr_ops.default_binder_kind,typ] , acc) , newenv)
       (concl,Global.env())
       (shift.funresprms2 @ shift.funresprms1
         @ shift.args2 @ shift.args1 @ shift.otherprms2 @ shift.otherprms1) in
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index e20beae963..5fc22cb4ad 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -187,7 +187,7 @@ GEXTEND Gram
   (* Tactic arguments to the right of an application *)
   tactic_arg_compat:
     [ [ a = tactic_arg -> a
-      | c = Constr.constr -> (match c with _loc, CRef (r,None) -> Reference r | c -> ConstrMayEval (ConstrTerm c))
+      | c = Constr.constr -> (match c with { CAst.v = CRef (r,None) } -> Reference r | c -> ConstrMayEval (ConstrTerm c))
       (* Unambiguous entries: tolerated w/o "ltac:" modifier *)
       | "()" -> TacGeneric (genarg_of_unit ()) ] ]
   ;
@@ -255,10 +255,10 @@ GEXTEND Gram
 	  let t, ty =
 	    match mpv with
 	    | Term t -> (match t with
-	      | _loc, CCast (t, (CastConv ty | CastVM ty | CastNative ty)) -> Term t, Some (Term ty)
+	      | { CAst.v = CCast (t, (CastConv ty | CastVM ty | CastNative ty)) } -> Term t, Some (Term ty)
 	      | _ -> mpv, None)
 	    | _ -> mpv, None
-	  in Def (na, t, Option.default (Term (Loc.tag @@ CHole (None, IntroAnonymous, None))) ty)
+	  in Def (na, t, Option.default (Term (CAst.make @@ CHole (None, IntroAnonymous, None))) ty)
     ] ]
   ;
   match_context_rule:
@@ -353,7 +353,7 @@ GEXTEND Gram
   operconstr: LEVEL "0"
     [ [ IDENT "ltac"; ":"; "("; tac = Pltac.tactic_expr; ")" ->
           let arg = Genarg.in_gen (Genarg.rawwit Tacarg.wit_tactic) tac in
-          Loc.tag ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ]
+          CAst.make ~loc:!@loc @@ CHole (None, IntroAnonymous, Some arg) ] ]
   ;
   END
 
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index 8aaad05666..60deb443a9 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -130,14 +130,14 @@ let mk_fix_tac (loc,id,bl,ann,ty) =
           (try List.index Names.Name.equal (snd x) ids
           with Not_found -> error "No such fix variable.")
       | _ -> error "Cannot guess decreasing argument of fix." in
-  (id,n, Loc.tag ~loc @@ CProdN(bl,ty))
+  (id,n, CAst.make ~loc @@ CProdN(bl,ty))
 
 let mk_cofix_tac (loc,id,bl,ann,ty) =
   let _ = Option.map (fun (aloc,_) ->
     user_err ~loc:aloc
       ~hdr:"Constr:mk_cofix_tac"
       (Pp.str"Annotation forbidden in cofix expression.")) ann in
-  (id,Loc.tag ~loc @@ CProdN(bl,ty))
+  (id,CAst.make ~loc @@ CProdN(bl,ty))
 
 (* Functions overloaded by quotifier *)
 let destruction_arg_of_constr (c,lbind as clbind) = match lbind with
@@ -154,12 +154,12 @@ let mkTacCase with_evar = function
   (* Reinterpret numbers as a notation for terms *)
   | [(clear,ElimOnAnonHyp n),(None,None),None],None ->
       TacCase (with_evar,
-        (clear,(Loc.tag @@ CPrim (Numeral (Bigint.of_int n)),
+        (clear,(CAst.make @@ CPrim (Numeral (Bigint.of_int n)),
 	 NoBindings)))
   (* Reinterpret ident as notations for variables in the context *)
   (* because we don't know if they are quantified or not *)
   | [(clear,ElimOnIdent id),(None,None),None],None ->
-      TacCase (with_evar,(clear,(Loc.tag @@ CRef (Ident id,None),NoBindings)))
+      TacCase (with_evar,(clear,(CAst.make @@ CRef (Ident id,None),NoBindings)))
   | ic ->
       if List.exists (function ((_, ElimOnAnonHyp _),_,_) -> true | _ -> false) (fst ic)
       then
@@ -169,7 +169,7 @@ let mkTacCase with_evar = function
 let rec mkCLambdaN_simple_loc ?loc bll c =
   match bll with
   | ((loc1,_)::_ as idl,bk,t) :: bll ->
-      Loc.tag ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
+      CAst.make ?loc @@ CLambdaN ([idl,bk,t],mkCLambdaN_simple_loc ?loc:(Loc.merge_opt loc1 loc) bll c)
   | ([],_,_) :: bll -> mkCLambdaN_simple_loc ?loc bll c
   | [] -> c
 
@@ -440,7 +440,7 @@ GEXTEND Gram
       | -> true ]]
   ;
   simple_binder:
-    [ [ na=name -> ([na],Default Explicit, Loc.tag ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
+    [ [ na=name -> ([na],Default Explicit, CAst.make ~loc:!@loc @@ CHole (Some (Evar_kinds.BinderType (snd na)), IntroAnonymous, None))
       | "("; nal=LIST1 name; ":"; c=lconstr; ")" -> (nal,Default Explicit,c)
     ] ]
   ;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index bdafbdc78c..58473d7ddf 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -340,7 +340,7 @@ type 'a extra_genarg_printer =
 
   let strip_prod_binders_expr n ty =
     let rec strip_ty acc n ty =
-      match snd ty with
+      match ty.CAst.v with
           Constrexpr.CProdN(bll,a) ->
             let nb =
               List.fold_left (fun i (nal,_,_) -> i + List.length nal) 0 bll in
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 19c2eaf0a7..2ef435b6ba 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -1787,18 +1787,18 @@ let rec strategy_of_ast = function
 
 (* By default the strategy for "rewrite_db" is top-down *)
 
-let mkappc s l = Loc.tag @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
+let mkappc s l = CAst.make @@ CAppExpl ((None,(Libnames.Ident (Loc.tag @@ Id.of_string s)),None),l)
 
 let declare_an_instance n s args =
   (((Loc.tag @@ Name n),None), Explicit,
-  Loc.tag @@ CAppExpl ((None, Qualid (Loc.tag @@  qualid_of_string s),None),
+  CAst.make @@ CAppExpl ((None, Qualid (Loc.tag @@  qualid_of_string s),None),
 	   args))
 
 let declare_instance a aeq n s = declare_an_instance n s [a;aeq]
 
 let anew_instance global binders instance fields =
   new_instance (Flags.is_universe_polymorphism ()) 
-    binders instance (Some (true, Loc.tag @@ CRecord (fields)))
+    binders instance (Some (true, CAst.make @@ CRecord (fields)))
     ~global ~generalize:false ~refine:false Hints.empty_hint_info
 
 let declare_instance_refl global binders a aeq n lemma =
@@ -1859,7 +1859,7 @@ let declare_relation ?(binders=[]) a aeq n refl symm trans =
 	     (Ident (Loc.tag @@ Id.of_string "Equivalence_Symmetric"), lemma2);
 	     (Ident (Loc.tag @@ Id.of_string "Equivalence_Transitive"), lemma3)])
 
-let cHole = Loc.tag @@ CHole (None, Misctypes.IntroAnonymous, None)
+let cHole = CAst.make @@ CHole (None, Misctypes.IntroAnonymous, None)
 
 let proper_projection sigma r ty =
   let rel_vect n m = Array.init m (fun i -> mkRel(n+m-i)) in
@@ -2012,13 +2012,13 @@ let add_morphism glob binders m s n =
   let instance_id = add_suffix n "_Proper" in
   let instance =
     (((Loc.tag @@ Name instance_id),None), Explicit,
-    Loc.tag @@ CAppExpl (
+    CAst.make @@ CAppExpl (
 	     (None, Qualid (Loc.tag @@ Libnames.qualid_of_string "Coq.Classes.Morphisms.Proper"),None),
 	     [cHole; s; m]))
   in
   let tac = Tacinterp.interp (make_tactic "add_morphism_tactic") in
     ignore(new_instance ~global:glob poly binders instance 
-	     (Some (true, Loc.tag @@ CRecord []))
+	     (Some (true, CAst.make @@ CRecord []))
 	      ~generalize:false ~tac ~hook:(declare_projection n instance_id) Hints.empty_hint_info)
 
 (** Bind to "rewrite" too *)
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 44ea3ff1d6..566dd8ed7b 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -108,13 +108,13 @@ let intern_ltac_variable ist = function
 
 let intern_constr_reference strict ist = function
   | Ident (_,id) as r when not strict && find_hyp id ist ->
-      (Loc.tag @@ GVar id), Some (Loc.tag @@ CRef (r,None))
+      (Loc.tag @@ GVar id), Some (CAst.make @@ CRef (r,None))
   | Ident (_,id) as r when find_var id ist ->
-      (Loc.tag @@ GVar id), if strict then None else Some (Loc.tag @@ CRef (r,None))
+      (Loc.tag @@ GVar id), if strict then None else Some (CAst.make @@ CRef (r,None))
   | r ->
       let loc,_ as lqid = qualid_of_reference r in
       Loc.tag @@ GRef (locate_global_with_alias lqid,None), 
-	if strict then None else Some (Loc.tag @@ CRef (r,None))
+	if strict then None else Some (CAst.make @@ CRef (r,None))
 
 let intern_move_location ist = function
   | MoveAfter id -> MoveAfter (intern_hyp ist id)
@@ -271,7 +271,7 @@ 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 (Loc.tag @@ CRef (Ident (Loc.tag id), None)) with
+	match intern_constr ist (CAst.make @@ CRef (Ident (Loc.tag id), None)) with
 	| (loc, GVar id), _ -> clear,ElimOnIdent (loc,id)
 	| c -> clear,ElimOnConstr (c,NoBindings)
       else
@@ -361,7 +361,7 @@ let intern_typed_pattern_or_ref_with_occurrences ist (l,p) =
           Inr (bound_names,(c,None),dummy_pat) in
   (l, match p with
   | Inl r -> interp_ref r
-  | Inr (_, CAppExpl((None,r,None),[])) ->
+  | Inr { CAst.v = CAppExpl((None,r,None),[]) } ->
       (* We interpret similarly @ref and ref *)
       interp_ref (AN r)
   | Inr c ->
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 4d5b844550..449027b52e 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -1072,7 +1072,7 @@ let interp_destruction_arg ist gl arg =
 	if Tactics.is_quantified_hypothesis id gl then
           keep,ElimOnIdent (loc,id)
 	else
-          let c = (Loc.tag ?loc @@ GVar id,Some (Loc.tag @@ CRef (Ident (loc,id),None))) in
+          let c = (Loc.tag ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in
           let f = { delayed = fun env sigma ->
             let sigma = Sigma.to_evar_map sigma in
             let (sigma,c) = interp_open_constr ist env sigma c in
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 0bc3f502ca..c11c9f83b7 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -148,15 +148,15 @@ let add_genarg tag pr =
 (** Constructors for cast type *)
 let dC t = CastConv t
 (** Constructors for constr_expr *)
-let isCVar   = function _loc, CRef (Ident _, _) -> true | _ -> false
-let destCVar = function _loc, CRef (Ident (_, id), _) -> id | _ ->
+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 mkCHole ~loc = Loc.tag ?loc @@ CHole (None, IntroAnonymous, None)
-let mkCLambda ?loc name ty t = Loc.tag ?loc @@
+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)
-let mkCLetIn ?loc name bo t = Loc.tag ?loc @@
+let mkCLetIn ?loc name bo t = CAst.make ?loc @@
    CLetIn ((Loc.tag ?loc name), bo, None, t)
-let mkCCast ?loc t ty = Loc.tag ?loc @@ CCast (t, dC ty)
+let mkCCast ?loc t ty = CAst.make ?loc @@ CCast (t, dC ty)
 (** Constructors for rawconstr *)
 let mkRHole = Loc.tag @@ GHole (InternalHole, IntroAnonymous, None)
 let mkRApp f args = if args = [] then f else Loc.tag @@ GApp (f, args)
@@ -951,7 +951,7 @@ let glob_cpattern gs p =
   | _, (_, None) as x -> x
   | k, (v, Some t) as orig ->
      if k = 'x' then glob_ssrterm gs ('(', (v, Some t)) else
-     match snd (Loc.to_pair t) with
+     match t.CAst.v with
      | CNotation("( _ in _ )", ([t1; t2], [], [])) ->
          (try match glob t1, glob t2 with
          | (r1, None), (r2, None) -> encode k "In" [r1;r2]
@@ -1019,9 +1019,9 @@ let pr_rpattern = pr_pattern
 type pattern = Evd.evar_map * (constr, constr) ssrpattern
 
 
-let id_of_cpattern = function
-  | _,(_,Some (_loc, CRef (Ident (_, x), _))) -> Some x
-  | _,(_,Some (_loc, CAppExpl ((_, Ident (_, x), _), []))) -> Some x
+let id_of_cpattern = let open CAst in function
+  | _,(_,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
@@ -1377,7 +1377,7 @@ let pf_fill_occ_term gl occ t =
 let cpattern_of_id id = ' ', (Loc.tag @@ GRef (VarRef  id, None), None)
 
 let is_wildcard : cpattern -> bool = function
-  | _,(_,Some (_, CHole _)| (_, GHole _),None) -> true
+  | _,(_,Some { CAst.v = CHole _ } | (_, GHole _),None) -> true
   | _ -> false
 
 (* "ssrpattern" *)