[ast] Improve precision of Ast location recognition in serialization.

We follow the suggestions in #402 and turn uses of `Loc.located` in
`vernac` into `CAst.t`. The impact should be low as this change mostly
affects top-level vernaculars.

With this change, we are even closer to automatically map a text
document to its AST in a programmatic way.

4 files changed, 43 insertions, 45 deletions

diff --git a/intf/constrexpr.ml b/intf/constrexpr.ml
index c59828794..5b51953bb 100644
--- a/intf/constrexpr.ml
+++ b/intf/constrexpr.ml
@@ -46,7 +46,7 @@ type prim_token =
 type instance_expr = Misctypes.glob_level list
 
 type cases_pattern_expr_r =
-  | CPatAlias of cases_pattern_expr * Name.t Loc.located
+  | CPatAlias of cases_pattern_expr * lname
   | CPatCstr  of reference
     * cases_pattern_expr list option * cases_pattern_expr list
   (** [CPatCstr (_, c, Some l1, l2)] represents (@c l1) l2 *)
@@ -68,14 +68,14 @@ and cases_pattern_notation_substitution =
 
 and constr_expr_r =
   | CRef     of reference * instance_expr option
-  | CFix     of Id.t Loc.located * fix_expr list
-  | CCoFix   of Id.t Loc.located * cofix_expr list
+  | CFix     of lident * fix_expr list
+  | CCoFix   of lident * cofix_expr list
   | CProdN   of local_binder_expr list * constr_expr
   | CLambdaN of local_binder_expr list * constr_expr
-  | CLetIn   of Name.t Loc.located * constr_expr * constr_expr option * constr_expr
+  | CLetIn   of lname * constr_expr * constr_expr option * constr_expr
   | CAppExpl of (proj_flag * reference * instance_expr option) * constr_expr list
   | CApp     of (proj_flag * constr_expr) *
-                (constr_expr * explicitation Loc.located option) list
+                (constr_expr * explicitation CAst.t option) list
   | CRecord  of (reference * constr_expr) list
 
   (* representation of the "let" and "match" constructs *)
@@ -84,9 +84,9 @@ and constr_expr_r =
             * case_expr list
             * branch_expr list    (* branches *)
 
-  | CLetTuple of Name.t Loc.located list * (Name.t Loc.located option * constr_expr option) *
+  | CLetTuple of lname list * (lname option * constr_expr option) *
                  constr_expr * constr_expr
-  | CIf of constr_expr * (Name.t Loc.located option * constr_expr option)
+  | CIf of constr_expr * (lname option * constr_expr option)
          * constr_expr * constr_expr
   | CHole   of Evar_kinds.t option * intro_pattern_naming_expr * Genarg.raw_generic_argument option
   | CPatVar of patvar
@@ -101,18 +101,18 @@ and constr_expr_r =
 and constr_expr = constr_expr_r CAst.t
 
 and case_expr = constr_expr                 (* expression that is being matched *)
-	      * Name.t Loc.located option   (* as-clause *)
+              * lname option                (* as-clause *)
 	      * cases_pattern_expr option   (* in-clause *)
 
 and branch_expr =
-  (cases_pattern_expr list list * constr_expr) Loc.located
+  (cases_pattern_expr list list * constr_expr) CAst.t
 
 and fix_expr =
-    Id.t Loc.located * (Id.t Loc.located option * recursion_order_expr) *
+    lident * (lident option * recursion_order_expr) *
       local_binder_expr list * constr_expr * constr_expr
 
 and cofix_expr =
-    Id.t Loc.located * local_binder_expr list * constr_expr * constr_expr
+    lident * local_binder_expr list * constr_expr * constr_expr
 
 and recursion_order_expr =
   | CStructRec
@@ -121,9 +121,9 @@ and recursion_order_expr =
 
 (** Anonymous defs allowed ?? *)
 and local_binder_expr =
-  | CLocalAssum   of Name.t Loc.located list * binder_kind * constr_expr
-  | CLocalDef     of Name.t Loc.located * constr_expr * constr_expr option
-  | CLocalPattern of (cases_pattern_expr * constr_expr option) Loc.located
+  | CLocalAssum   of lname list * binder_kind * constr_expr
+  | CLocalDef     of lname * constr_expr * constr_expr option
+  | CLocalPattern of (cases_pattern_expr * constr_expr option) CAst.t
 
 and constr_notation_substitution =
     constr_expr list *      (** for constr subterms *)
diff --git a/intf/genredexpr.ml b/intf/genredexpr.ml
index a8c37c620..bdf3242ca 100644
--- a/intf/genredexpr.ml
+++ b/intf/genredexpr.ml
@@ -8,8 +8,6 @@
 
 (** Reduction expressions *)
 
-open Names
-
 (** The parsing produces initially a list of [red_atom] *)
 
 type 'a red_atom =
@@ -52,7 +50,7 @@ type ('a,'b,'c) red_expr_gen =
 type ('a,'b,'c) may_eval =
   | ConstrTerm of 'a
   | ConstrEval of ('a,'b,'c) red_expr_gen * 'a
-  | ConstrContext of Id.t Loc.located * 'a
+  | ConstrContext of Misctypes.lident * 'a
   | ConstrTypeOf of 'a
 
 open Libnames
diff --git a/intf/misctypes.ml b/intf/misctypes.ml
index 33e961419..aafd61b3c 100644
--- a/intf/misctypes.ml
+++ b/intf/misctypes.ml
@@ -8,7 +8,13 @@
 
 open Names
 
-(** Basic types used both in [constr_expr] and in [glob_constr] *)
+(** Basic types used both in [constr_expr], [glob_constr], and [vernacexpr] *)
+
+(** Located identifiers and objects with syntax. *)
+
+type lident = Id.t CAst.t
+type lname = Name.t CAst.t
+type lstring = string CAst.t
 
 (** Cases pattern variables *)
 
@@ -101,9 +107,9 @@ type 'a with_bindings = 'a * 'a bindings
 
 type 'a or_var =
   | ArgArg of 'a
-  | ArgVar of Names.Id.t Loc.located
+  | ArgVar of lident
 
-type 'a and_short_name = 'a * Id.t Loc.located option
+type 'a and_short_name = 'a * lident option
 
 type 'a or_by_notation =
   | AN of 'a
@@ -134,7 +140,7 @@ type multi =
 
 type 'a core_destruction_arg =
   | ElimOnConstr of 'a
-  | ElimOnIdent of Id.t Loc.located
+  | ElimOnIdent of lident
   | ElimOnAnonHyp of int
 
 type 'a destruction_arg =
diff --git a/intf/vernacexpr.ml b/intf/vernacexpr.ml
index d16c9bb80..ba28eacea 100644
--- a/intf/vernacexpr.ml
+++ b/intf/vernacexpr.ml
@@ -6,19 +6,12 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Loc
 open Names
 open Misctypes
 open Constrexpr
-open Decl_kinds
 open Libnames
 
 (** Vernac expressions, produced by the parser *)
-
-type lident = Id.t located
-type lname = Name.t located
-type lstring = string located
-
 type class_rawexpr = FunClass | SortClass | RefClass of reference or_by_notation
 
 (* spiwack: I'm choosing, for now, to have [goal_selector] be a
@@ -40,7 +33,8 @@ type goal_reference =
   | NthGoal of int
   | GoalId of Id.t
 
-type univ_name_list = Name.t Loc.located list
+type univ_name_list = Universes.univ_name_list
+[@@ocaml.deprecated "Use [Universes.univ_name_list]"]
 
 type printable =
   | PrintTables
@@ -56,7 +50,7 @@ type printable =
   | PrintMLLoadPath
   | PrintMLModules
   | PrintDebugGC
-  | PrintName of reference or_by_notation * univ_name_list option
+  | PrintName of reference or_by_notation * Universes.univ_name_list option
   | PrintGraph
   | PrintClasses
   | PrintTypeClasses
@@ -72,7 +66,7 @@ type printable =
   | PrintScopes
   | PrintScope of string
   | PrintVisibility of string option
-  | PrintAbout of reference or_by_notation * univ_name_list option * goal_selector option
+  | PrintAbout of reference or_by_notation * Universes.univ_name_list option * goal_selector option
   | PrintImplicit of reference or_by_notation
   | PrintAssumptions of bool * bool * reference or_by_notation
   | PrintStrategy of reference or_by_notation option
@@ -164,7 +158,7 @@ type option_ref_value =
 
 (** Identifier and optional list of bound universes and constraints. *)
 
-type universe_decl_expr = (Id.t Loc.located list, glob_constraint list) gen_universe_decl
+type universe_decl_expr = (lident list, glob_constraint list) gen_universe_decl
 
 type ident_decl = lident * universe_decl_expr option
 type name_decl = lname * universe_decl_expr option
@@ -177,7 +171,7 @@ type definition_expr =
       * constr_expr option
 
 type fixpoint_expr =
-    ident_decl * (Id.t located option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
+    ident_decl * (lident option * recursion_order_expr) * local_binder_expr list * constr_expr * constr_expr option
 
 type cofixpoint_expr =
     ident_decl * local_binder_expr list * constr_expr * constr_expr option
@@ -205,7 +199,7 @@ type inductive_expr =
 type one_inductive_expr =
   ident_decl * local_binder_expr list * constr_expr option * constructor_expr list
 
-type typeclass_constraint = name_decl * binding_kind * constr_expr
+type typeclass_constraint = name_decl * Decl_kinds.binding_kind * constr_expr
 
 and typeclass_context = typeclass_constraint list
 
@@ -221,7 +215,7 @@ type syntax_modifier =
   | SetOnlyParsing
   | SetOnlyPrinting
   | SetCompatVersion of Flags.compat_version
-  | SetFormat of string * string located
+  | SetFormat of string * lstring
 
 type proof_end =
   | Admitted
@@ -321,7 +315,7 @@ type vernac_implicit_status = Implicit | MaximallyImplicit | NotImplicit
 type vernac_argument_status = {
   name : Name.t;
   recarg_like : bool;
-  notation_scope : string Loc.located option;
+  notation_scope : string CAst.t option;
   implicit_status : vernac_implicit_status;
 }
 
@@ -341,15 +335,15 @@ type nonrec vernac_expr =
   | VernacNotationAddFormat of string * string * string
 
   (* Gallina *)
-  | VernacDefinition of (discharge * definition_object_kind) * name_decl * definition_expr
-  | VernacStartTheoremProof of theorem_kind * proof_expr list
+  | VernacDefinition of (Decl_kinds.discharge * Decl_kinds.definition_object_kind) * name_decl * definition_expr
+  | VernacStartTheoremProof of Decl_kinds.theorem_kind * proof_expr list
   | VernacEndProof of proof_end
   | VernacExactProof of constr_expr
-  | VernacAssumption of (discharge * assumption_object_kind) *
+  | VernacAssumption of (Decl_kinds.discharge * Decl_kinds.assumption_object_kind) *
       inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of cumulative_inductive_parsing_flag * private_flag * inductive_flag * (inductive_expr * decl_notation list) list
-  | VernacFixpoint of discharge * (fixpoint_expr * decl_notation list) list
-  | VernacCoFixpoint of discharge * (cofixpoint_expr * decl_notation list) list
+  | VernacInductive of cumulative_inductive_parsing_flag * Decl_kinds.private_flag * inductive_flag * (inductive_expr * decl_notation list) list
+  | VernacFixpoint of Decl_kinds.discharge * (fixpoint_expr * decl_notation list) list
+  | VernacCoFixpoint of Decl_kinds.discharge * (cofixpoint_expr * decl_notation list) list
   | VernacScheme of (lident option * scheme) list
   | VernacCombinedScheme of lident * lident list
   | VernacUniverse of lident list
@@ -416,7 +410,7 @@ type nonrec vernac_expr =
   | VernacCreateHintDb of string * bool
   | VernacRemoveHints of string list * reference list
   | VernacHints of string list * hints_expr
-  | VernacSyntacticDefinition of Id.t located * (Id.t list * constr_expr) *
+  | VernacSyntacticDefinition of lident * (Id.t list * constr_expr) *
       onlyparsing_flag
   | VernacDeclareImplicits of reference or_by_notation *
       (explicitation * bool * bool) list list
@@ -482,8 +476,8 @@ type vernac_control =
   | VernacExpr of vernac_flag list * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
-  | VernacTime of bool * vernac_control located
-  | VernacRedirect of string * vernac_control located
+  | VernacTime of bool * vernac_control CAst.t
+  | VernacRedirect of string * vernac_control CAst.t
   | VernacTimeout of int * vernac_control
   | VernacFail of vernac_control