From 0b0f75b427c8c95ac31a77b29725e6cd7fb16482 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Wed, 14 Dec 2016 13:38:15 -0500 Subject: Work around bug in 8.4 implicits --- src/Reflection/Syntax.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'src') diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v index 42d04c3de..2a6cce891 100644 --- a/src/Reflection/Syntax.v +++ b/src/Reflection/Syntax.v @@ -294,7 +294,7 @@ Section language. : interp_flat_type_gen var' t -> flat_type := @smart_interp_flat_map var' (fun _ => flat_type) f (fun _ _ => Prod) t. Fixpoint SmartFlatTypeMapInterp {var' var''} (f : forall t, var' t -> base_type_code) - (fv : forall t v, var'' (f t v)) {t} {struct t} + (fv : forall t v, var'' (f t v)) t {struct t} : forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) with | Tbase x => fv _ -- cgit v1.2.3