From 80d0cf475af29fc011da4415967a460a32cafb73 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sun, 30 Oct 2016 21:54:22 -0400 Subject: Fix tactic notation scope in the 8.5 build --- src/Reflection/Z/Interpretations.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index 0c9a18c79..3c0eb0309 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -521,7 +521,7 @@ Module Relations. | progress intros | progress destruct_head' prod | progress destruct_head' and - | progress specialize_by ltac:(exact I) + | progress specialize_by (exact I) | progress subst | progress break_match | progress break_match_hyps -- cgit v1.2.3