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.
---
 tactics/equality.ml | 2 +-
 tactics/tactics.ml  | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'tactics')

diff --git a/tactics/equality.ml b/tactics/equality.ml
index 674d01777d..9a1ac768c7 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -1484,7 +1484,7 @@ let simpleInjClause flags with_evars = function
   | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c
 
 let injConcl flags = injClause flags None false None
-let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
+let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent CAst.(make id)))
 
 let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter begin fun gl ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 29a30b4a22..7e281e2fe0 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1190,7 +1190,7 @@ let onOpenInductionArg env sigma tac = function
              let sigma = Tacmach.New.project gl in
              tac clear_flag (sigma,(c,NoBindings))
              end))
-  | clear_flag,ElimOnIdent (_,id) ->
+  | clear_flag,ElimOnIdent {CAst.v=id} ->
       (* A quantified hypothesis *)
       Tacticals.New.tclTHEN
         (try_intros_until_id_check id)
@@ -1206,7 +1206,7 @@ let onInductionArg tac = function
       Tacticals.New.tclTHEN
         (intros_until_n n)
         (Tacticals.New.onLastHyp (fun c -> tac clear_flag (c,NoBindings)))
-  | clear_flag,ElimOnIdent (_,id) ->
+  | clear_flag,ElimOnIdent {CAst.v=id} ->
       (* A quantified hypothesis *)
       Tacticals.New.tclTHEN
         (try_intros_until_id_check id)
-- 
cgit v1.2.3