Fix a bad line

1 files changed, 1 insertions, 1 deletions

diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 45ab931cb..3660c6705 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -121,7 +121,7 @@ Section language.
            | Tbase _ => val _
            | Prod A B => (@SmartVal T val A, @SmartVal T val B)
            end.
-        := @smart_interp_flat_map _ (interp_flat_type_gen exprf) (fun t => Const) (fun A B x y => pair x y) t.
+
       (** [SmartVar] is like [Var], except that it inserts
           pair-projections and [Pair] as necessary to handle
           [flat_type], and not just [base_type_code] *)