From ee2197096fe75a63b4d92cb3a1bb05122c5c625b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Sun, 9 Apr 2017 03:35:20 +0200 Subject: [location] [ast] Port module AST to CAst --- plugins/ltac/g_rewrite.ml4 | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/ltac/g_rewrite.ml4') diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index 1f40c67b5..b4a0e46ae 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ TACTIC EXTEND rewrite_strat END let clsubstitute o c = - let is_tac id = match fst (fst (snd c)) with (_, GVar id') when Id.equal id' id -> true | _ -> false in + let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id'} when Id.equal id' id -> true | _ -> false in Tacticals.onAllHypsAndConcl (fun cl -> match cl with -- cgit v1.2.3