diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-10-30 21:54:22 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-10-30 21:54:22 -0400 |
| commit | 80d0cf475af29fc011da4415967a460a32cafb73 (patch) | |
| tree | 729ffb1b424248b172abbd448e1a46f72beec025 /src | |
| parent | cf71d9060d90d3d25e899eb1d8473681152e4695 (diff) | |
Fix tactic notation scope in the 8.5 build
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Interpretations.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 |