diff options
| author | Emilio Jesus Gallego Arias | 2017-12-10 09:26:25 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-02-22 00:44:33 +0100 |
| commit | 9bebbb96e58b3c1b0f7f88ba2af45462eae69b0f (patch) | |
| tree | 24e8de17078242c1ea39e31ecfe55a1c024d0eff /pretyping | |
| parent | 0c5f0afffd37582787f79267d9841259095b7edc (diff) | |
[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.
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/univdecls.ml | 7 | ||||
| -rw-r--r-- | pretyping/univdecls.mli | 2 |
2 files changed, 4 insertions, 5 deletions
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 |