Split off some bits of Reflection.Syntax

Also split off some bits of Util.Tactics

2 files changed, 3 insertions, 2 deletions

diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v
index 7822985e1..bd9a46b9a 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -1,6 +1,7 @@
 (** * Compute a list of liveness values for each binding *)
 Require Import Coq.Lists.List.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.CountLets.
 Require Import Crypto.Util.ListUtil.
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index f6ce5d1f5..2c1f3bd23 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -1,6 +1,7 @@
 (** * Named Representation of Gallina *)
 Require Import Coq.Classes.RelationClasses.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
@@ -54,7 +55,7 @@ Module Export Named.
           pair-projections and [Pair] as necessary to handle
           [flat_type], and not just [base_type_code] *)
         Definition SmartVar {t} : interp_flat_type_gen (fun _ => Name) t -> exprf t
-          := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) _ (fun t => Var) TT (fun A B x y => Pair x y).
+          := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) (fun t => Var) TT (fun A B x y => Pair x y).
       End expr.
 
       Section with_context.
@@ -88,7 +89,6 @@ Module Export Named.
         Definition lookup (ctx : Context) {t}
           : interp_flat_type_gen (fun _ => Name) t -> option (interp_flat_type_gen var t)
           := smart_interp_flat_map
-               base_type_code
                (g := fun t => option (interp_flat_type_gen var t))
                (fun t v => lookupb ctx v)
                (Some tt)