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

5 files changed, 14 insertions, 14 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 54ba19d6a..03ff580ad 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -416,7 +416,7 @@ let qhyp_eq h1 h2 = match h1, h2 with
 | _ -> false
 
 let check_bindings bl =
-  match List.duplicates qhyp_eq (List.map (fun x -> fst (snd x)) bl) with
+  match List.duplicates qhyp_eq (List.map (fun {CAst.v=x} -> fst x) bl) with
     | NamedHyp s :: _ ->
 	user_err 
 	  (str "The variable " ++ Id.print s ++
@@ -512,7 +512,7 @@ let clenv_match_args bl clenv =
     let mvs = clenv_independent clenv in
     check_bindings bl;
     List.fold_left
-      (fun clenv (loc,(b,c)) ->
+      (fun clenv {CAst.loc;v=(b,c)} ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
           if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
@@ -710,7 +710,7 @@ let solve_evar_clause env sigma hyp_only clause = function
     error_not_right_number_missing_arguments len
 | ExplicitBindings lbind ->
   let () = check_bindings lbind in
-  let fold sigma (_, (binder, c)) =
+  let fold sigma {CAst.v=(binder, c)} =
     let ev = evar_of_binder clause.cl_holes binder in
     define_with_type sigma env ev c
   in
diff --git a/proofs/miscprint.ml b/proofs/miscprint.ml
index e363af644..1a63ff673 100644
--- a/proofs/miscprint.ml
+++ b/proofs/miscprint.ml
@@ -14,7 +14,7 @@ open Misctypes
 
 (** Printing of [intro_pattern] *)
 
-let rec pr_intro_pattern prc (_,pat) = match pat with
+let rec pr_intro_pattern prc {CAst.v=pat} = match pat with
   | IntroForthcoming true -> str "*"
   | IntroForthcoming false -> str "**"
   | IntroNaming p -> pr_intro_pattern_naming p
@@ -31,7 +31,7 @@ and pr_intro_pattern_action prc = function
   | IntroInjection pl ->
       str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++
       str "]"
-  | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
+  | IntroApplyOn ({CAst.v=c},pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c
   | IntroRewrite true -> str "->"
   | IntroRewrite false -> str "<-"
 
@@ -52,9 +52,9 @@ let pr_move_location pr_id = function
   | MoveLast -> str " at bottom"
 
 (** Printing of bindings *)
-let pr_binding prc = function
-  | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
-  | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
+let pr_binding prc = let open CAst in function
+  | {loc;v=(NamedHyp id, c)} -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c)
+  | {loc;v=(AnonHyp n, c)} -> hov 1 (int n ++ str " := " ++ cut () ++ prc c)
 
 let pr_bindings prc prlc = function
   | ImplicitBindings l ->
diff --git a/proofs/miscprint.mli b/proofs/miscprint.mli
index 762d7cc87..79790a277 100644
--- a/proofs/miscprint.mli
+++ b/proofs/miscprint.mli
@@ -13,7 +13,7 @@ open Misctypes
 (** Printing of [intro_pattern] *)
 
 val pr_intro_pattern :
-  ('a -> Pp.t) -> 'a intro_pattern_expr Loc.located -> Pp.t
+  ('a -> Pp.t) -> 'a intro_pattern_expr CAst.t -> Pp.t
 
 val pr_or_and_intro_pattern :
   ('a -> Pp.t) -> 'a or_and_intro_pattern_expr -> Pp.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 15f34ccc6..d6c0e3341 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -207,7 +207,7 @@ let check_no_pending_proof () =
 let discard_gen id =
   pstates := List.filter (fun { pid = id' } -> not (Id.equal id id')) !pstates
 
-let discard (loc,id) =
+let discard {CAst.loc;v=id} =
   let n = List.length !pstates in
   discard_gen id;
   if Int.equal (List.length !pstates) n then
@@ -297,13 +297,13 @@ let set_used_variables l =
     match entry with
     | LocalAssum (x,_) ->
        if Id.Set.mem x all_safe then orig
-       else (ctx, all_safe, (Loc.tag x)::to_clear) 
+       else (ctx, all_safe, (CAst.make x)::to_clear)
     | LocalDef (x,bo, ty) as decl ->
        if Id.Set.mem x all_safe then orig else
        let vars = Id.Set.union (vars_of env bo) (vars_of env ty) in
        if Id.Set.subset vars all_safe
        then (decl :: ctx, Id.Set.add x all_safe, to_clear)
-       else (ctx, all_safe, (Loc.tag x) :: to_clear) in
+       else (ctx, all_safe, (CAst.make x) :: to_clear) in
   let ctx, _, to_clear =
     Environ.fold_named_context aux env ~init:(ctx,ctx_set,[]) in
   let to_clear = if !proof_using_auto_clear then to_clear else [] in
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index fb123fccb..bf35fd659 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -22,7 +22,7 @@ val check_no_pending_proof : unit -> unit
 val get_current_proof_name : unit -> Names.Id.t
 val get_all_proof_names : unit -> Names.Id.t list
 
-val discard : Names.Id.t Loc.located -> unit
+val discard : Misctypes.lident -> unit
 val discard_current : unit -> unit
 val discard_all : unit -> unit
 
@@ -124,7 +124,7 @@ val set_endline_tactic : Genarg.glob_generic_argument -> unit
  * (w.r.t. type dependencies and let-ins covered by it) + a list of
  * ids to be cleared *)
 val set_used_variables :
-  Names.Id.t list -> Context.Named.t * Names.Id.t Loc.located list
+  Names.Id.t list -> Context.Named.t * Misctypes.lident list
 val get_used_variables : unit -> Context.Named.t option
 
 (** Get the universe declaration associated to the current proof. *)