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. --- plugins/ltac/tauto.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/ltac/tauto.ml') diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml index 01d3f79c7..5ce30c3d7 100644 --- a/plugins/ltac/tauto.ml +++ b/plugins/ltac/tauto.ml @@ -255,10 +255,10 @@ let tauto_power_flags = { } let with_flags flags _ ist = - let f = (Loc.tag @@ Id.of_string "f") in - let x = (Loc.tag @@ Id.of_string "x") in + let f = CAst.make @@ Id.of_string "f" in + let x = CAst.make @@ Id.of_string "x" in let arg = Val.Dyn (tag_tauto_flags, flags) in - let ist = { ist with lfun = Id.Map.add (snd x) arg ist.lfun } in + let ist = { ist with lfun = Id.Map.add x.CAst.v arg ist.lfun } in eval_tactic_ist ist (TacArg (Loc.tag @@ TacCall (Loc.tag (ArgVar f, [Reference (ArgVar x)])))) let register_tauto_tactic tac name0 args = -- cgit v1.2.3