[located] More work towards using CAst.t

We continue with the work of #402 and #6745 and update most of the
remaining parts of the AST:

- module declarations
- intro patterns
- top-level sentences

Now, parsed documents should be full annotated by `CAst` nodes.

8 files changed, 44 insertions, 45 deletions

diff --git a/interp/constrextern.ml b/interp/constrextern.ml
index 9efaff3b9..f5a6a082e 100644
--- a/interp/constrextern.ml
+++ b/interp/constrextern.ml
@@ -850,7 +850,7 @@ let rec extern inctx scopes vars r =
                    | Name _, _ -> Some (CAst.make na) in
                  (sub_extern false scopes vars tm,
                   na',
-                  Option.map (fun (loc,(ind,nal)) ->
+                  Option.map (fun {CAst.loc;v=(ind,nal)} ->
                               let args = List.map (fun x -> DAst.make @@ PatVar x) nal in
                               let fullargs = add_cpatt_for_params ind args in
                               extern_ind_pattern_in_scope scopes vars ind fullargs
@@ -929,7 +929,7 @@ and factorize_prod scopes vars na bk aty c =
   | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
          when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
     (match get () with
-     | [(_,(ids,disj_of_patl,b))] ->
+     | [{CAst.v=(ids,disj_of_patl,b)}] ->
       let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = extern_typ scopes vars b in
@@ -957,7 +957,7 @@ and factorize_lambda inctx scopes vars na bk aty c =
   | Name id, GCases (LetPatternStyle, None, [(e,(Anonymous,None))],(_::_ as eqns))
          when is_gvar id e && List.length (store (factorize_eqns eqns)) = 1 ->
     (match get () with
-     | [(_,(ids,disj_of_patl,b))] ->
+     | [{CAst.v=(ids,disj_of_patl,b)}] ->
       let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
       let disjpat = if occur_glob_constr id b then List.map (set_pat_alias id) disjpat else disjpat in
       let b = sub_extern inctx scopes vars b in
@@ -1010,7 +1010,7 @@ and extern_local_binder scopes vars = function
       let (assums,ids,l) = extern_local_binder scopes vars l in
       (assums,ids, CLocalPattern(CAst.make @@ (p,ty)) :: l)
 
-and extern_eqn inctx scopes vars (loc,(ids,pll,c)) =
+and extern_eqn inctx scopes vars {CAst.loc;v=(ids,pll,c)} =
   let pll = List.map (List.map (extern_cases_pattern_in_scope scopes vars)) pll in
   make ?loc (pll,extern inctx scopes vars c)
 
@@ -1155,7 +1155,7 @@ let extern_closed_glob ?lax goal_concl_style env sigma t =
 
 let any_any_branch =
   (* | _ => _ *)
-  Loc.tag ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
+  CAst.make ([],[DAst.make @@ PatVar Anonymous], DAst.make @@ GHole (Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None))
 
 let compute_displayed_name_in_pattern sigma avoid na c =
   let open Namegen in
diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 918e12e5c..55b943eac 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -524,7 +524,7 @@ let rec expand_binders ?loc mk bl c =
      | GLocalPattern ((disjpat,ids), id, bk, ty) ->
         let tm = DAst.make ?loc (GVar id) in
         (* Distribute the disjunctive patterns over the shared right-hand side *)
-        let eqnl = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in
+        let eqnl = List.map (fun pat -> CAst.make ?loc (ids,[pat],c)) disjpat in
         let c = DAst.make ?loc @@ GCases (Misctypes.LetPatternStyle, None, [tm,(Anonymous,None)], eqnl) in
         expand_binders ?loc mk bl (mk ?loc (Name id,Explicit,ty) c)
 
@@ -1954,14 +1954,14 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
              let thevars, thepats = List.split l in
              let sub_rtn = (* Some (GSort (Loc.ghost,GType None)) *) None in
              let sub_tms = List.map (fun id -> (DAst.make @@ GVar id),(Name id,None)) thevars (* "match v1,..,vn" *) in
-             let main_sub_eqn = Loc.tag @@
+             let main_sub_eqn = CAst.make @@
                ([],thepats, (* "|p1,..,pn" *)
 		Option.cata (intern_type env')
                   (DAst.make ?loc @@ GHole(Evar_kinds.CasesType false,Misctypes.IntroAnonymous,None))
                   rtnpo) (* "=> P" if there were a return predicate P, and "=> _" otherwise *) in
              let catch_all_sub_eqn =
                if List.for_all (irrefutable globalenv) thepats then [] else
-                  [Loc.tag @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
+                  [CAst.make @@ ([],List.make (List.length thepats) (DAst.make @@ PatVar Anonymous), (* "|_,..,_" *)
                    DAst.make @@ GHole(Evar_kinds.ImpossibleCase,Misctypes.IntroAnonymous,None))]   (* "=> _" *) in
              Some (DAst.make @@ GCases(Term.RegularStyle,sub_rtn,sub_tms,main_sub_eqn::catch_all_sub_eqn))
 	in
@@ -2077,7 +2077,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
     List.map (fun (asubst,pl) ->
       let rhs = replace_vars_constr_expr asubst rhs in
       let rhs' = intern {env with ids = env_ids} rhs in
-      (loc,(eqn_ids,pl,rhs'))) pll
+      CAst.make ?loc (eqn_ids,pl,rhs')) pll
 
   and intern_case_item env forbidden_names_for_gen (tm,na,t) =
     (* the "match" part *)
@@ -2110,7 +2110,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
 	    match case_rel_ctxt,arg_pats with
 	      (* LetIn in the rel_context *)
 	      | LocalDef _ :: t, l when not with_letin ->
-		canonize_args t l forbidden_names match_acc ((Loc.tag Anonymous)::var_acc)
+                canonize_args t l forbidden_names match_acc ((CAst.make Anonymous)::var_acc)
 	      | [],[] ->
 		(add_name match_acc na, var_acc)
 	      | (LocalAssum (cano_name,ty) | LocalDef (cano_name,_,ty)) :: t, c::tt ->
@@ -2118,21 +2118,21 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
                 | PatVar x ->
                   let loc = c.CAst.loc in
                   canonize_args t tt forbidden_names
-                    (add_name match_acc CAst.(make ?loc x)) ((loc,x)::var_acc)
+                    (add_name match_acc CAst.(make ?loc x)) (CAst.make ?loc x::var_acc)
                 | _ ->
                   let fresh =
                     Namegen.next_name_away_with_default_using_types "iV" cano_name forbidden_names (EConstr.of_constr ty) in
                   canonize_args t tt (Id.Set.add fresh forbidden_names)
-                    ((fresh,c)::match_acc) ((cases_pattern_loc c,Name fresh)::var_acc)
+                    ((fresh,c)::match_acc) ((CAst.make ?loc:(cases_pattern_loc c) @@ Name fresh)::var_acc)
                 end
 	      | _ -> assert false in
 	  let _,args_rel =
 	    List.chop nparams (List.rev mip.Declarations.mind_arity_ctxt) in
 	  canonize_args args_rel l forbidden_names_for_gen [] [] in
-	match_to_do, Some (cases_pattern_expr_loc t,(ind,List.rev_map snd nal))
+        match_to_do, Some (CAst.make ?loc:(cases_pattern_expr_loc t) (ind,List.rev_map (fun x -> x.v) nal))
     | None ->
       [], None in
-    (tm',(na.CAst.v,typ)), extra_id, match_td
+    (tm',(na.CAst.v, typ)), extra_id, match_td
 
   and intern_impargs c env l subscopes args =
     let eargs, rargs = extract_explicit_arg l args in
@@ -2164,7 +2164,7 @@ let internalize globalenv env pattern_mode (_, ntnvars as lvar) c =
       | (imp::impl', []) ->
 	  if not (Id.Map.is_empty eargs) then
 	    (let (id,(loc,_)) = Id.Map.choose eargs in
-	       user_err ?loc  (str "Not enough non implicit \
+               user_err ?loc (str "Not enough non implicit \
 	    arguments to accept the argument bound to " ++
 		 Id.print id ++ str"."));
 	  []
diff --git a/interp/modintern.ml b/interp/modintern.ml
index 887685585..dc93d8dc4 100644
--- a/interp/modintern.ml
+++ b/interp/modintern.ml
@@ -45,7 +45,7 @@ let error_application_to_module_type loc =
     or both are searched. The returned kind is never ModAny, and
     it is equal to the input kind when this one isn't ModAny. *)
 
-let lookup_module_or_modtype kind (loc,qid) =
+let lookup_module_or_modtype kind {CAst.loc;v=qid} =
   try
     if kind == ModType then raise Not_found;
     let mp = Nametab.locate_module qid in
@@ -60,9 +60,9 @@ let lookup_module_or_modtype kind (loc,qid) =
 let lookup_module lqid = fst (lookup_module_or_modtype Module lqid)
 
 let transl_with_decl env = function
-  | CWith_Module ((_,fqid),qid) ->
+  | CWith_Module ({CAst.v=fqid},qid) ->
       WithMod (fqid,lookup_module qid), Univ.ContextSet.empty
-  | CWith_Definition ((_,fqid),udecl,c) ->
+  | CWith_Definition ({CAst.v=fqid},udecl,c) ->
     let sigma, udecl = Univdecls.interp_univ_decl_opt env udecl in
     let c, ectx = interp_constr env sigma c in
     begin match UState.check_univ_decl ~poly:(Flags.is_universe_polymorphism()) ectx udecl with
@@ -81,11 +81,11 @@ let loc_of_module l = l.CAst.loc
 (* Invariant : the returned kind is never ModAny, and it is
    equal to the input kind when this one isn't ModAny. *)
 
-let rec interp_module_ast env kind m cst = match m.CAst.v with
-  | CMident qid ->
-      let (mp,kind) = lookup_module_or_modtype kind (m.CAst.loc,qid) in
+let rec interp_module_ast env kind m cst = match m with
+  | {CAst.loc;v=CMident qid} ->
+      let (mp,kind) = lookup_module_or_modtype kind CAst.(make ?loc qid) in
       (MEident mp, kind, cst)
-  | CMapply (me1,me2) ->
+  | {CAst.loc;v=CMapply (me1,me2)} ->
       let me1',kind1, cst = interp_module_ast env kind me1 cst in
       let me2',kind2, cst = interp_module_ast env ModAny me2 cst in
       let mp2 = match me2' with
@@ -95,7 +95,7 @@ let rec interp_module_ast env kind m cst = match m.CAst.v with
       if kind2 == ModType then
         error_application_to_module_type (loc_of_module me2);
       (MEapply (me1',mp2), kind1, cst)
-  | CMwith (me,decl) ->
+  | {CAst.loc;v=CMwith (me,decl)} ->
       let me,kind,cst = interp_module_ast env kind me cst in
       if kind == Module then error_incorrect_with_in_module m.CAst.loc;
       let decl, cst' = transl_with_decl env decl in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 77ef601b7..a0d69ce79 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -156,7 +156,7 @@ let protect g e na =
 
 let apply_cases_pattern ?loc ((ids,disjpat),id) c =
   let tm = DAst.make ?loc (GVar id) in
-  let eqns = List.map (fun pat -> (loc,(ids,[pat],c))) disjpat in
+  let eqns = List.map (fun pat -> (CAst.make ?loc (ids,[pat],c))) disjpat in
   DAst.make ?loc @@ GCases (LetPatternStyle, None, [tm,(Anonymous,None)], eqns)
 
 let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
@@ -192,7 +192,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
 	  let e',nal' = List.fold_right (fun na (e',nal) ->
               let e',na' = protect g e' na in
               e',na'::nal) nal (e',[]) in
-          e',Some (Loc.tag ?loc (ind,nal')) in
+          e',Some (CAst.make ?loc (ind,nal')) in
         let e',na' = protect g e' na in
         (e',(f e tm,(na',t'))::tml')) tml (e,[]) in
       let fold (idl,e) na = let (e,disjpat,na) = g e na in ((Name.cons na idl,e),disjpat,na) in
@@ -200,7 +200,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc =
         let ((idl,e),patl) =
           List.fold_left_map (cases_pattern_fold_map ?loc fold) ([],e) patl in
         let disjpatl = product_of_cases_patterns patl in
-        List.map (fun patl -> Loc.tag (idl,patl,f e rhs)) disjpatl) eqnl in
+        List.map (fun patl -> CAst.make (idl,patl,f e rhs)) disjpatl) eqnl in
       GCases (sty,Option.map (f e') rtntypopt,tml',List.flatten eqnl')
   | NLetTuple (nal,(na,po),b,c) ->
       let e',nal = List.fold_left_map (protect g) e nal in
@@ -411,13 +411,13 @@ let notation_constr_and_vars_of_glob_constr recvars a =
   | GProd (na,bk,ty,c) -> add_name found na; NProd (na,aux ty,aux c)
   | GLetIn (na,b,t,c) -> add_name found na; NLetIn (na,aux b,Option.map aux t, aux c)
   | GCases (sty,rtntypopt,tml,eqnl) ->
-      let f (_,(idl,pat,rhs)) = List.iter (add_id found) idl; (pat,aux rhs) in
+      let f {CAst.v=(idl,pat,rhs)} = List.iter (add_id found) idl; (pat,aux rhs) in
       NCases (sty,Option.map aux rtntypopt,
         List.map (fun (tm,(na,x)) ->
 	  add_name found na;
 	  Option.iter
-	    (fun (_,(_,nl)) -> List.iter (add_name found) nl) x;
-          (aux tm,(na,Option.map (fun (_,(ind,nal)) -> (ind,nal)) x))) tml,
+            (fun {CAst.v=(_,nl)} -> List.iter (add_name found) nl) x;
+          (aux tm,(na,Option.map (fun {CAst.v=(ind,nal)} -> (ind,nal)) x))) tml,
         List.map f eqnl)
   | GLetTuple (nal,(na,po),b,c) ->
       add_name found na;
@@ -661,7 +661,7 @@ let abstract_return_type_context pi mklam tml rtno =
     rtno
 
 let abstract_return_type_context_glob_constr tml rtn =
-  abstract_return_type_context (fun (_,(_,nal)) -> nal)
+  abstract_return_type_context (fun {CAst.v=(_,nal)} -> nal)
     (fun na c -> DAst.make @@
       GLambda(na,Explicit,DAst.make @@ GHole(Evar_kinds.InternalHole,Misctypes.IntroAnonymous,None),c)) tml rtn
 
@@ -1241,7 +1241,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
   | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
        when is_gvar p e && is_bindinglist_meta id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
     (match get () with
-     | [(_,(ids,disj_of_patl,b1))] ->
+     | [{CAst.v=(ids,disj_of_patl,b1)}] ->
      let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
      let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in
      let alp,sigma = bind_bindinglist_env alp sigma id [DAst.make ?loc @@ GLocalPattern ((disjpat,ids),p,bk,t)] in
@@ -1250,7 +1250,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
   | Name p, GCases (LetPatternStyle,None,[(e,_)],(_::_ as eqns)), Name id
        when is_gvar p e && is_onlybinding_pattern_like_meta false id metas && List.length (store (Detyping.factorize_eqns eqns)) = 1 ->
     (match get () with
-     | [(_,(ids,disj_of_patl,b1))] ->
+     | [{CAst.v=(ids,disj_of_patl,b1)}] ->
      let disjpat = List.map (function [pat] -> pat | _ -> assert false) disj_of_patl in
      let disjpat = if occur_glob_constr p b1 then List.map (set_pat_alias p) disjpat else disjpat in
      let alp,sigma = bind_binding_env alp sigma id disjpat in
@@ -1263,7 +1263,7 @@ and match_extended_binders ?loc isprod u alp metas na1 na2 bk t sigma b1 b2 =
      let (alp,sigma) = match_names metas (alp,sigma) na1 na2 in
      match_in u alp metas sigma b1 b2
 
-and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 rest2 =
+and match_equations u alp metas sigma {CAst.v=(ids,patl1,rhs1)} (patl2,rhs2) rest1 rest2 =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
   let allow_catchall = (rest2 = [] && ids = []) in
@@ -1272,7 +1272,7 @@ and match_equations u alp metas sigma (_,(ids,patl1,rhs1)) (patl2,rhs2) rest1 re
       (alp,sigma) patl1 patl2 in
   match_in u alp metas sigma rhs1 rhs2
 
-and match_disjunctive_equations u alp metas sigma (_,(ids,disjpatl1,rhs1)) (disjpatl2,rhs2) _ _ =
+and match_disjunctive_equations u alp metas sigma {CAst.v=(ids,disjpatl1,rhs1)} (disjpatl2,rhs2) _ _ =
   (* patl1 and patl2 have the same length because they respectively
      correspond to some tml1 and tml2 that have the same length *)
   let (alp,sigma) =
diff --git a/interp/smartlocate.ml b/interp/smartlocate.ml
index bc24a19de..6033d509b 100644
--- a/interp/smartlocate.ml
+++ b/interp/smartlocate.ml
@@ -68,16 +68,16 @@ let global_with_alias ?head r =
 let smart_global ?head = function
   | AN r ->
       global_with_alias ?head r
-  | ByNotation (loc,(ntn,sc)) ->
+  | ByNotation {CAst.loc;v=(ntn,sc)} ->
       Notation.interp_notation_as_global_reference ?loc (fun _ -> true) ntn sc
 
 let smart_global_inductive = function
   | AN r ->
       global_inductive_with_alias r
-  | ByNotation (loc,(ntn,sc)) ->
+  | ByNotation {CAst.loc;v=(ntn,sc)} ->
       destIndRef
         (Notation.interp_notation_as_global_reference ?loc isIndRef ntn sc)
 
 let loc_of_smart_reference = function
   | AN r -> loc_of_reference r
-  | ByNotation (loc,(_,_)) -> loc
+  | ByNotation {CAst.loc;v=(_,_)} -> loc
diff --git a/interp/stdarg.ml b/interp/stdarg.ml
index 5f1aad0c2..0958cc7ee 100644
--- a/interp/stdarg.ml
+++ b/interp/stdarg.ml
@@ -34,7 +34,7 @@ let wit_pre_ident : string uniform_genarg_type =
 
 let loc_of_or_by_notation f = function
   | AN c -> f c
-  | ByNotation (loc,(s,_)) -> loc
+  | ByNotation {CAst.loc;v=(s,_)} -> loc
 
 let wit_int_or_var =
   make0 ~dyn:(val_tag (topwit wit_int)) "int_or_var"
diff --git a/interp/stdarg.mli b/interp/stdarg.mli
index 948ec1381..b69129956 100644
--- a/interp/stdarg.mli
+++ b/interp/stdarg.mli
@@ -39,7 +39,7 @@ val wit_pre_ident : string uniform_genarg_type
 
 val wit_int_or_var : (int or_var, int or_var, int) genarg_type
 
-val wit_intro_pattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_intro_pattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
 
 val wit_ident : Id.t uniform_genarg_type
 
@@ -88,7 +88,7 @@ val wit_reference : (reference, global_reference located or_var, global_referenc
 val wit_global : (reference, global_reference located or_var, global_reference) genarg_type
 val wit_clause :  (lident Locus.clause_expr, lident Locus.clause_expr, Names.Id.t Locus.clause_expr) genarg_type
 val wit_quantified_hypothesis : quantified_hypothesis uniform_genarg_type
-val wit_intropattern : (constr_expr intro_pattern_expr located, glob_constr_and_expr intro_pattern_expr located, intro_pattern) genarg_type
+val wit_intropattern : (constr_expr intro_pattern_expr CAst.t, glob_constr_and_expr intro_pattern_expr CAst.t, intro_pattern) genarg_type
 val wit_redexpr :
   ((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
   (glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) red_expr_gen,
diff --git a/interp/tactypes.ml b/interp/tactypes.ml
index fc0f8de5f..83e42be89 100644
--- a/interp/tactypes.ml
+++ b/interp/tactypes.ml
@@ -12,7 +12,6 @@
     lower API. It's not clear whether this is a temporary API or if this is
     meant to stay. *)
 
-open Loc
 open Names
 open Constrexpr
 open Pattern
@@ -29,7 +28,7 @@ type 'a delayed_open = Environ.env -> Evd.evar_map -> Evd.evar_map * 'a
 type delayed_open_constr = EConstr.constr delayed_open
 type delayed_open_constr_with_bindings = EConstr.constr with_bindings delayed_open
 
-type intro_pattern = delayed_open_constr intro_pattern_expr located
-type intro_patterns = delayed_open_constr intro_pattern_expr located list
-type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr located
-type intro_pattern_naming = intro_pattern_naming_expr located
+type intro_pattern = delayed_open_constr intro_pattern_expr CAst.t
+type intro_patterns = delayed_open_constr intro_pattern_expr CAst.t list
+type or_and_intro_pattern = delayed_open_constr or_and_intro_pattern_expr CAst.t
+type intro_pattern_naming = intro_pattern_naming_expr CAst.t