Add interp_type_gen_rel_pointwise2, *_gen => *

6 files changed, 8 insertions, 7 deletions

diff --git a/src/Reflection/Named/Compile.v b/src/Reflection/Named/Compile.v
index e37815597..973b2b2e7 100644
--- a/src/Reflection/Named/Compile.v
+++ b/src/Reflection/Named/Compile.v
@@ -19,7 +19,7 @@ Section language.
   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 interp_flat_type := (interp_flat_type_gen interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type interp_base_type).
   Local Notation exprf := (@exprf base_type_code interp_base_type op (fun _ => Name)).
   Local Notation expr := (@expr base_type_code interp_base_type op (fun _ => Name)).
   Local Notation nexprf := (@Named.exprf base_type_code interp_base_type op Name).
diff --git a/src/Reflection/Named/DeadCodeElimination.v b/src/Reflection/Named/DeadCodeElimination.v
index 1b2fa3fc0..a2b39347c 100644
--- a/src/Reflection/Named/DeadCodeElimination.v
+++ b/src/Reflection/Named/DeadCodeElimination.v
@@ -26,7 +26,7 @@ Section language.
   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 interp_flat_type := (interp_flat_type_gen interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type interp_base_type).
   Local Notation exprf := (@exprf base_type_code interp_base_type op (fun _ => Name)).
   Local Notation expr := (@expr base_type_code interp_base_type op (fun _ => Name)).
   Local Notation Expr := (@Expr base_type_code interp_base_type op).
diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v
index 2301eb6a1..b9d283013 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -37,7 +37,7 @@ Section language.
   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 interp_flat_type := (interp_flat_type_gen interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type interp_base_type).
   Local Notation exprf := (@exprf base_type_code interp_base_type op).
   Local Notation expr := (@expr base_type_code interp_base_type op).
 
diff --git a/src/Reflection/Named/NameUtil.v b/src/Reflection/Named/NameUtil.v
index bab860585..d9ef0f9b1 100644
--- a/src/Reflection/Named/NameUtil.v
+++ b/src/Reflection/Named/NameUtil.v
@@ -11,8 +11,8 @@ Section language.
     Context (MName : Type) (force : MName -> option Name).
     Fixpoint split_mnames
              (t : flat_type base_type_code) (ls : list MName)
-      : option (interp_flat_type_gen (fun _ => Name) t) * list MName
-      := match t return option (@interp_flat_type_gen base_type_code (fun _ => Name) t) * _ with
+      : option (interp_flat_type (fun _ => Name) t) * list MName
+      := match t return option (@interp_flat_type base_type_code (fun _ => Name) t) * _ with
          | Syntax.Tbase _
            => match ls with
               | cons n ls'
diff --git a/src/Reflection/Named/RegisterAssign.v b/src/Reflection/Named/RegisterAssign.v
index 5736d01a3..749019fa4 100644
--- a/src/Reflection/Named/RegisterAssign.v
+++ b/src/Reflection/Named/RegisterAssign.v
@@ -19,7 +19,7 @@ Section language.
   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 interp_flat_type := (interp_flat_type_gen interp_base_type).
+  Local Notation interp_flat_type := (interp_flat_type interp_base_type).
   Local Notation exprf := (@exprf base_type_code interp_base_type op).
   Local Notation expr := (@expr base_type_code interp_base_type op).
 
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index 70925c16b..0ea950325 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -34,7 +34,8 @@ Module Export Named.
     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 interp_flat_type := (interp_flat_type_gen interp_base_type).
+    Local Notation interp_flat_type_gen := interp_flat_type.
+    Local Notation interp_flat_type := (interp_flat_type interp_base_type).
 
 
     Section expr_param.