diff options
| author |  Jason Gross <jgross@mit.edu> | 2016-12-14 13:38:15 -0500 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2016-12-14 13:38:15 -0500 |
| commit | 0b0f75b427c8c95ac31a77b29725e6cd7fb16482 (patch) | |
| tree | d55f82b1c7c8a20db95854db262cea10e35b7467 /src/Reflection/Syntax.v | |
| parent | 356f43e29f1da80fb34035d72eeeadac238210d8 (diff) | |
Work around bug in 8.4 implicits
Diffstat (limited to 'src/Reflection/Syntax.v')
| -rw-r--r-- | src/Reflection/Syntax.v | 2 |
1 files changed, 1 insertions, 1 deletions
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 _ |