From c812d93d1356ce6a752f56ac1f7d96d6ae342252 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 4 Nov 2016 14:28:33 -0400 Subject: Fix implicits of Let for 8.4 --- src/Reflection/Z/Interpretations.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/Reflection') diff --git a/src/Reflection/Z/Interpretations.v b/src/Reflection/Z/Interpretations.v index f9b767b66..f4812a76e 100644 --- a/src/Reflection/Z/Interpretations.v +++ b/src/Reflection/Z/Interpretations.v @@ -623,21 +623,21 @@ Module Relations. {t : type base_type} : interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop := match t return interp_type interp_base_type1 t -> interp_type interp_base_type2 t -> Prop with - | Tflat T => R + | Tflat T => @R _ | Arrow A B => fun f g => forall x : interp_flat_type interp_base_type1 (all_binders_for (Arrow A B)), let y := SmartVarfMap proj x in let fx := ApplyInterpedAll f x in let gy := ApplyInterpedAll g y in - R fx gy + @R _ fx gy end. Lemma uncurry_interp_type_rel_pointwise2_proj {t : type base_type} {f : interp_type interp_base_type1 t} {g} - : interp_type_rel_pointwise2 (t:=t) (fun t => R) f g + : interp_type_rel_pointwise2 (t:=t) (fun t => @R _) f g -> interp_type_rel_pointwise2_uncurried_proj (t:=t) f g. Proof. unfold interp_type_rel_pointwise2_uncurried_proj. -- cgit v1.2.3