[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.

6 files changed, 24 insertions, 24 deletions

diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index 21d1339c5..90af20b4c 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -68,9 +68,9 @@ let pr_intro_as_pat _prc _ _ pat =
         str"<simple_intropattern>"
     | None -> mt ()
 
-let out_disjunctive = function
-  | loc, IntroAction (IntroOrAndPattern l) -> (loc,l)
-  | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected.")
+let out_disjunctive = CAst.map (function
+  | IntroAction (IntroOrAndPattern l) -> l
+  | _ -> CErrors.user_err Pp.(str "Disjunctive or conjunctive intro pattern expected."))
 
 ARGUMENT EXTEND with_names TYPED AS intropattern_opt PRINTED BY pr_intro_as_pat
 |   [ "as"  simple_intropattern(ipat) ] -> [ Some ipat ]
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 7159614d9..49f7aae43 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -287,7 +287,7 @@ let make_discr_match_el  =
 *)
 let make_discr_match_brl i =
   List.map_i
-    (fun j (_,(idl,patl,_)) -> Loc.tag @@
+    (fun j {CAst.v=(idl,patl,_)} -> CAst.make @@
        if Int.equal j i
        then (idl,patl, mkGRef (Lazy.force coq_True_ref))
        else (idl,patl, mkGRef (Lazy.force coq_False_ref))
@@ -659,7 +659,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	assert (Int.equal (Array.length case_pats) 2);
 	let brl =
 	  List.map_i
-	    (fun i x -> Loc.tag ([],[case_pats.(i)],x))
+            (fun i x -> CAst.make ([],[case_pats.(i)],x))
 	    0
 	    [lhs;rhs]
 	in
@@ -689,7 +689,7 @@ let rec build_entry_lc env funnames avoid rt : glob_constr build_entry_return =
 	  in
 	  let case_pats = build_constructors_of_type (fst ind) nal_as_glob_constr in
 	  assert (Int.equal (Array.length case_pats) 1);
-	  let br = Loc.tag ([],[case_pats.(0)],e) in
+          let br = CAst.make ([],[case_pats.(0)],e) in
 	  let match_expr = mkGCases(None,[b,(Anonymous,None)],[br]) in
 	  build_entry_lc env funnames avoid match_expr
 
@@ -756,7 +756,7 @@ and build_entry_lc_from_case_term env types funname make_discr patterns_to_preve
     | [] -> (* computed_branches  *) {result = [];to_avoid = avoid}
     | br::brl' ->
 	(* alpha conversion to prevent name clashes *)
-	let _,(idl,patl,return) = alpha_br avoid br in
+        let {CAst.v=(idl,patl,return)} = alpha_br avoid br in
 	let new_avoid  = idl@avoid in 	(* for now we can no more use idl as an identifier *)
 	(* building a list of precondition stating that we are not in this branch
 	   (will be used in the following recursive calls)
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 41eb48657..40ea40b6b 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -111,11 +111,11 @@ let change_vars =
 		Miscops.map_cast_type (change_vars mapping) c)
       | GProj(p,c) -> GProj(p, change_vars mapping c)
       ) rt
-  and change_vars_br mapping ((loc,(idl,patl,res)) as br) =
+  and change_vars_br mapping ({CAst.loc;v=(idl,patl,res)} as br) =
     let new_mapping = List.fold_right Id.Map.remove idl mapping in
     if Id.Map.is_empty new_mapping
     then br
-    else (loc,(idl,patl,change_vars new_mapping res))
+    else CAst.make ?loc (idl,patl,change_vars new_mapping res)
   in
   change_vars
 
@@ -298,13 +298,13 @@ let rec alpha_rt excluded rt =
   in
   new_rt
 
-and alpha_br excluded (loc,(ids,patl,res)) =
+and alpha_br excluded {CAst.loc;v=(ids,patl,res)} =
   let new_patl,new_excluded,mapping = alpha_patl excluded patl in
   let new_ids = List.fold_right raw_get_pattern_id new_patl [] in
   let new_excluded = new_ids@excluded in
   let renamed_res = change_vars mapping res in
   let new_res = alpha_rt new_excluded renamed_res in
-  (loc,(new_ids,new_patl,new_res))
+  CAst.make ?loc (new_ids,new_patl,new_res)
 
 (*
    [is_free_in id rt] checks if [id] is a free variable in [rt]
@@ -348,7 +348,7 @@ let is_free_in id =
     | GCast (b,CastCoerce) -> is_free_in b
     | GProj (_,c) -> is_free_in c
     ) x
-  and is_free_in_br (_,(ids,_,rt)) =
+  and is_free_in_br {CAst.v=(ids,_,rt)} =
     (not (Id.List.mem id ids)) && is_free_in rt
   in
   is_free_in
@@ -443,10 +443,10 @@ let replace_var_by_term x_id term =
       | GProj(p,c) ->
         GProj(p,replace_var_by_pattern c)
     ) x
-  and replace_var_by_pattern_br ((loc,(idl,patl,res)) as br) =
+  and replace_var_by_pattern_br ({CAst.loc;v=(idl,patl,res)} as br) =
     if List.exists (fun id -> Id.compare id x_id == 0) idl
     then br
-    else (loc,(idl,patl,replace_var_by_pattern res))
+    else CAst.make ?loc (idl,patl,replace_var_by_pattern res)
   in
   replace_var_by_pattern
 
@@ -547,8 +547,8 @@ let expand_as =
 		List.map (expand_as_br map) brl)
       | GProj(p,c) -> GProj(p, expand_as map c)
     )
-  and expand_as_br map (loc,(idl,cpl,rt)) =
-    (loc,(idl,cpl, expand_as (List.fold_left add_as map cpl) rt))
+  and expand_as_br map {CAst.loc; v=(idl,cpl,rt)} =
+    CAst.make ?loc (idl,cpl, expand_as (List.fold_left add_as map cpl) rt)
   in
   expand_as Id.Map.empty
 
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 13eda3952..1c27b27e2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -215,7 +215,7 @@ let is_rec names =
 	List.exists (fun (e,_) -> lookup names e) el ||
 	  List.exists (lookup_br names) brl
     | GProj(_,c) -> lookup names c
-  and lookup_br names (_,(idl,_,rt)) =
+  and lookup_br names {CAst.v=(idl,_,rt)} =
     let new_names = List.fold_right Id.Set.remove idl names in
     lookup new_names rt
   in
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b858e78d0..2743a8a2f 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -240,7 +240,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       List.map
 	(fun decl ->
 	   List.map
-	     (fun id -> Loc.tag @@ IntroNaming (IntroIdentifier id))
+             (fun id -> CAst.make @@ IntroNaming (IntroIdentifier id))
 	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
@@ -256,7 +256,7 @@ let prove_fun_correct evd funs_constr graphs_constr schemes lemmas_types_infos i
       (* We get the identifiers of this branch *)
       let pre_args =
       	List.fold_right
-      	  (fun (_,pat) acc ->
+          (fun {CAst.v=pat} acc ->
       	     match pat with
 	       | IntroNaming (IntroIdentifier id) -> id::acc
       	       | _ -> anomaly (Pp.str "Not an identifier.")
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 759c88633..4cbcde8e5 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -206,7 +206,7 @@ let (value_f: Constr.t list -> global_reference -> Constr.t) =
 	(RegularStyle,None,
 	 [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], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
+         [CAst.make ([v_id], [DAst.make @@ PatCstr ((destIndRef (delayed_force coq_sig_ref),1),
 			   [DAst.make @@ PatVar(Name v_id); DAst.make @@ PatVar Anonymous],
                            Anonymous)],
 	    DAst.make @@ GVar v_id)])
@@ -899,8 +899,8 @@ let rec make_rewrite_list expr_info max = function
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
-	     ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr);
-                              Loc.tag @@ (NamedHyp k, f_S max)]) false) g) )
+             ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
+                              CAst.make @@ (NamedHyp k, f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
@@ -926,8 +926,8 @@ let make_rewrite expr_info l hp max =
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
 	    (mkVar hp,
-	     ExplicitBindings[Loc.tag @@ (NamedHyp def, expr_info.f_constr);
-                              Loc.tag @@ (NamedHyp k, f_S (f_S max))]) false)) g)
+             ExplicitBindings[CAst.make @@ (NamedHyp def, expr_info.f_constr);
+                              CAst.make @@ (NamedHyp k, f_S (f_S max))]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (observe_tclTHENLIST (str "make_rewrite")[