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

3 files changed, 11 insertions, 11 deletions

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index 31f811bc8..fda31756a 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -143,8 +143,8 @@ type constr_pattern_expr = constr_expr
 (** Concrete syntax for modules and module types *)
 
 type with_declaration_ast =
-  | CWith_Module of Id.t list Loc.located * qualid Loc.located
-  | CWith_Definition of Id.t list Loc.located * universe_decl_expr option * constr_expr
+  | CWith_Module of Id.t list CAst.t * qualid CAst.t
+  | CWith_Definition of Id.t list CAst.t * universe_decl_expr option * constr_expr
 
 type module_ast_r =
   | CMident of qualid
diff --git a/intf/glob_term.ml b/intf/glob_term.ml
index 39a7b956a..84be15552 100644
--- a/intf/glob_term.ml
+++ b/intf/glob_term.ml
@@ -72,14 +72,14 @@ and 'a fix_kind_g =
   | GCoFix of int
 
 and 'a predicate_pattern_g =
-    Name.t * (inductive * Name.t list) Loc.located option
+    Name.t * (inductive * Name.t list) CAst.t option
       (** [(na,id)] = "as 'na' in 'id'" where if [id] is [Some(l,I,k,args)]. *)
 
 and 'a tomatch_tuple_g = ('a glob_constr_g * 'a predicate_pattern_g)
 
 and 'a tomatch_tuples_g = 'a tomatch_tuple_g list
 
-and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) Loc.located
+and 'a cases_clause_g = (Id.t list * 'a cases_pattern_g list * 'a glob_constr_g) CAst.t
 (** [(p,il,cl,t)] = "|'cl' => 't'". Precondition: the free variables
     of [t] are members of [il]. *)
 and 'a cases_clauses_g = 'a cases_clause_g list
@@ -96,7 +96,7 @@ type fix_recursion_order = [ `any ] fix_recursion_order_g
 
 type any_glob_constr = AnyGlobConstr : 'r glob_constr_g -> any_glob_constr
 
-type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) Loc.located
+type 'a disjunctive_cases_clause_g = (Id.t list * 'a cases_pattern_g list list * 'a glob_constr_g) CAst.t
 type 'a disjunctive_cases_clauses_g = 'a disjunctive_cases_clause_g list
 type 'a cases_pattern_disjunction_g = 'a cases_pattern_g list
 
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 54a4861d0..1eee3dfc7 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -35,12 +35,12 @@ and intro_pattern_naming_expr =
 and 'constr intro_pattern_action_expr =
   | IntroWildcard
   | IntroOrAndPattern of 'constr or_and_intro_pattern_expr
-  | IntroInjection of ('constr intro_pattern_expr) Loc.located list
-  | IntroApplyOn of 'constr Loc.located * 'constr intro_pattern_expr Loc.located
+  | IntroInjection of ('constr intro_pattern_expr) CAst.t list
+  | IntroApplyOn of 'constr CAst.t * 'constr intro_pattern_expr CAst.t
   | IntroRewrite of bool
 and 'constr or_and_intro_pattern_expr =
-  | IntroOrPattern of ('constr intro_pattern_expr) Loc.located list list
-  | IntroAndPattern of ('constr intro_pattern_expr) Loc.located list
+  | IntroOrPattern of ('constr intro_pattern_expr) CAst.t list list
+  | IntroAndPattern of ('constr intro_pattern_expr) CAst.t list
 
 (** Move destination for hypothesis *)
 
@@ -95,7 +95,7 @@ type 'a cast_type =
 
 type quantified_hypothesis = AnonHyp of int | NamedHyp of Id.t
 
-type 'a explicit_bindings = (quantified_hypothesis * 'a) Loc.located list
+type 'a explicit_bindings = (quantified_hypothesis * 'a) CAst.t list
 
 type 'a bindings =
   | ImplicitBindings of 'a list
@@ -115,7 +115,7 @@ type 'a and_short_name = 'a * lident option
 
 type 'a or_by_notation =
   | AN of 'a
-  | ByNotation of (string * string option) Loc.located
+  | ByNotation of (string * string option) CAst.t
 
 (* NB: the last string in [ByNotation] is actually a [Notation.delimiters],
    but this formulation avoids a useless dependency. *)