diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-11-09 15:55:17 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-11-09 15:55:17 -0500 |
| commit | c34c352bda727f9447b94471df3e14da5ec45399 (patch) | |
| tree | a7674769c69dd6775e389ba2da8dab8761962229 /src | |
| parent | 803106ed9b27337b564ba2d2fa860164e1cbdc69 (diff) | |
Fix for 8.4
Diffstat (limited to 'src')
| -rw-r--r-- | src/Reflection/Z/Interpretations/Relations.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Reflection/Z/Interpretations/Relations.v b/src/Reflection/Z/Interpretations/Relations.v index 4f33f48bb..963834a10 100644 --- a/src/Reflection/Z/Interpretations/Relations.v +++ b/src/Reflection/Z/Interpretations/Relations.v @@ -579,7 +579,7 @@ Proof. | progress (unfold proj_eq_rel in *; subst) | apply @related_tuples_None_left; constructor | apply -> @related_tuples_Some_left - | apply <- @related_tuples_proj_eq_rel_untuple + | refine (proj2 (@related_tuples_proj_eq_rel_untuple _ _ _ _ _ _) _) | apply <- @related_tuples_lift_relation2_untuple' | progress rewrite ?HList.map'_mapt', <- ?HList.map_is_mapt' | progress rewrite ?Tuple.map_map2, ?Tuple.map2_fst, ?Tuple.map2_snd, ?Tuple.map_id |