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/comProgramFixpoint.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'vernac/comProgramFixpoint.ml') diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index a9a91e304..af34f8b29 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -298,16 +298,16 @@ let do_program_recursive local poly fixkind fixl ntns = let do_program_fixpoint local poly l = let g = List.map (fun ((_,wf,_,_,_),_) -> wf) l in match g, l with - | [(n, CWfRec r)], [((((_,id),pl),_,bl,typ,def),ntn)] -> + | [(n, CWfRec r)], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> let recarg = match n with - | Some n -> mkIdentC (snd n) + | Some n -> mkIdentC n.CAst.v | None -> user_err ~hdr:"do_program_fixpoint" (str "Recursive argument required for well-founded fixpoints") in build_wellfounded (id, pl, n, bl, typ, out_def def) poly r recarg ntn - | [(n, CMeasureRec (m, r))], [((((_,id),pl),_,bl,typ,def),ntn)] -> + | [(n, CMeasureRec (m, r))], [((({CAst.v=id},pl),_,bl,typ,def),ntn)] -> build_wellfounded (id, pl, n, bl, typ, out_def def) poly (Option.default (CAst.make @@ CRef (lt_ref,None)) r) m ntn @@ -322,7 +322,7 @@ let do_program_fixpoint local poly l = let extract_cofixpoint_components l = let fixl, ntnl = List.split l in - List.map (fun (((_,id),pl),bl,typ,def) -> + List.map (fun (({CAst.v=id},pl),bl,typ,def) -> {fix_name = id; fix_annot = None; fix_univs = pl; fix_binders = bl; fix_body = def; fix_type = typ}) fixl, List.flatten ntnl -- cgit v1.2.3