From 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 10 Dec 2017 09:26:25 +0100
Subject: [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.
---
 pretyping/univdecls.ml  | 7 +++----
 pretyping/univdecls.mli | 2 +-
 2 files changed, 4 insertions(+), 5 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/univdecls.ml b/pretyping/univdecls.ml
index 3cf32d7ff0..89f1185a99 100644
--- a/pretyping/univdecls.ml
+++ b/pretyping/univdecls.ml
@@ -6,12 +6,11 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-open Names
 open CErrors
 
 (** Local universes and constraints declarations *)
 type universe_decl =
-  (Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
 let default_univ_decl =
   let open Misctypes in
@@ -34,9 +33,9 @@ let interp_univ_constraints env evd cstrs =
   in
   List.fold_left interp (evd,Univ.Constraint.empty) cstrs
 
-let interp_univ_decl env decl = 
+let interp_univ_decl env decl =
   let open Misctypes in
-  let pl = decl.univdecl_instance in
+  let pl : lident list = decl.univdecl_instance in
   let evd = Evd.from_ctx (Evd.make_evar_universe_context env (Some pl)) in
   let evd, cstrs = interp_univ_constraints env evd decl.univdecl_constraints in
   let decl = { univdecl_instance = pl;
diff --git a/pretyping/univdecls.mli b/pretyping/univdecls.mli
index 0c3b749cbf..706d3a157f 100644
--- a/pretyping/univdecls.mli
+++ b/pretyping/univdecls.mli
@@ -8,7 +8,7 @@
 
 (** Local universe and constraint declarations. *)
 type universe_decl =
-  (Names.Id.t Loc.located list, Univ.Constraint.t) Misctypes.gen_universe_decl
+  (Misctypes.lident list, Univ.Constraint.t) Misctypes.gen_universe_decl
 
 val default_univ_decl : universe_decl
 
-- 
cgit v1.2.3