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. --- vernac/classes.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'vernac/classes.ml') diff --git a/vernac/classes.ml b/vernac/classes.ml index 4a2dba859..695be74bb 100644 --- a/vernac/classes.ml +++ b/vernac/classes.ml @@ -132,7 +132,7 @@ let new_instance ?(abstract=false) ?(global=false) ?(refine= !refine_instance) ~program_mode poly ctx (instid, bk, cl) props ?(generalize=true) ?(tac:unit Proofview.tactic option) ?hook pri = let env = Global.env() in - let ((loc, instid), pl) = instid in + let ({CAst.loc;v=instid}, pl) = instid in let sigma, decl = Univdecls.interp_univ_decl_opt env pl in let tclass, ids = match bk with @@ -410,7 +410,7 @@ let context poly l = let nstatus = match b with | None -> pi3 (ComAssumption.declare_assumption false decl (t, univs) Universes.empty_binders [] impl - Vernacexpr.NoInline (Loc.tag id)) + Vernacexpr.NoInline (CAst.make id)) | Some b -> let decl = (Discharge, poly, Definition) in let entry = Declare.definition_entry ~univs ~types:t b in -- cgit v1.2.3