1 files changed, 17 insertions, 17 deletions
diff --git a/src/Reflection/FilterLive.v b/src/Reflection/FilterLive.v
index 446f9195c..57e296df7 100644
--- a/src/Reflection/FilterLive.v
+++ b/src/Reflection/FilterLive.v
@@ -9,7 +9,6 @@ Local Notation eta x := (fst x, snd x).
 Local Open Scope ctype_scope.
 Section language.
   Context (base_type_code : Type)
-          (interp_base_type : base_type_code -> Type)
           (op : flat_type base_type_code -> flat_type base_type_code -> Type)
           (Name : Type)
           (dead_name : Name)
@@ -20,13 +19,10 @@ Section language.
 
   Local Notation flat_type := (flat_type base_type_code).
   Local Notation type := (type base_type_code).
-  Let Tbase := @Tbase base_type_code.
-  Local Coercion Tbase : base_type_code >-> Syntax.flat_type.
-  Local Notation interp_type := (interp_type interp_base_type).
   Local Notation var := (fun t : base_type_code => list Name).
-  Local Notation exprf := (@exprf base_type_code interp_base_type op var).
-  Local Notation expr := (@expr base_type_code interp_base_type op var).
-  Local Notation Expr := (@Expr base_type_code interp_base_type op var).
+  Local Notation exprf := (@exprf base_type_code op var).
+  Local Notation expr := (@expr base_type_code op var).
+  Local Notation Expr := (@Expr base_type_code op var).
 
   Fixpoint merge_name_lists (ls1 ls2 : list Name) : list Name :=
     match ls1, ls2 with
@@ -36,11 +32,11 @@ Section language.
     end.
 
   Definition names_to_list {t} : interp_flat_type (fun _ => Name) t -> list Name
-    := smart_interp_flat_map base_type_code (g:=fun _ => list Name) (fun _ x => x :: nil)%list (fun _ _ x y => x ++ y)%list.
+    := smart_interp_flat_map base_type_code (g:=fun _ => list Name) (fun _ x => x :: nil)%list nil (fun _ _ x y => x ++ y)%list.
 
   Fixpoint filter_live_namesf (prefix remaining : list Name) {t} (e : exprf t) : list Name
     := match e with
-       | Const _ x => prefix
+       | TT => prefix
        | Var _ x => x
        | Op _ _ op args => @filter_live_namesf prefix remaining _ args
        | LetIn tx ex _ eC
@@ -58,13 +54,17 @@ Section language.
        end.
 
   Fixpoint filter_live_names (prefix remaining : list Name) {t} (e : expr t) : list Name
-    := match e, remaining with
-       | Return _ x, _ => filter_live_namesf prefix remaining x
-       | Abs src _ ef, cons n remaining'
-         => let prefix' := (prefix ++ (n :: nil))%list in
-            @filter_live_names
-              prefix' remaining' _
-              (ef prefix')
-       | Abs _ _ _, nil => nil
+    := match e with
+       | Return _ x => filter_live_namesf prefix remaining x
+       | Abs src _ ef
+         => let '(ns, remaining') := eta (split_names (Tbase src) remaining) in
+            match ns with
+            | Some n =>
+              let prefix' := (prefix ++ names_to_list n)%list in
+              @filter_live_names
+                prefix' remaining' _
+                (ef (SmartValf _ (fun _ => prefix') (Tbase src)))
+            | None => nil
+            end
        end.
 End language.