Better implicits for interpf, pointwise-lifting of rels over interp_type_gen

3 files changed, 11 insertions, 2 deletions

diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v
index 98faeaa44..4a5dc810b 100644
--- a/src/Reflection/InputSyntax.v
+++ b/src/Reflection/InputSyntax.v
@@ -90,7 +90,7 @@ Section language.
       Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
 
       Lemma compilef_correct {t} (e : @exprf interp_flat_type t)
-      : Syntax.interpf base_type_code interp_base_type op interp_op (compilef e) = interpf interp_op e.
+      : Syntax.interpf interp_op (compilef e) = interpf interp_op e.
       Proof.
         induction e;
           repeat match goal with
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index 5790178e7..2d4ad5e0f 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -16,7 +16,7 @@ Section language.
   Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
 
   Lemma interpf_SmartVar t v
-    : Syntax.interpf base_type_code interp_base_type op interp_op (SmartVar (t:=t) v) = v.
+    : Syntax.interpf interp_op (SmartVar (t:=t) v) = v.
   Proof.
     unfold SmartVar; induction t;
       repeat match goal with
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index cc816f58f..6d632342b 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -34,6 +34,15 @@ Section language.
         | Tflat t => interp_flat_type t
         | Arrow x y => (interp_flat_type x -> interp_type_gen y)%type
         end.
+      Section rel.
+        Context (R : forall t, interp_flat_type t -> interp_flat_type t -> Prop).
+        Fixpoint interp_type_gen_rel_pointwise (t : type)
+          : interp_type_gen t -> interp_type_gen t -> Prop :=
+          match t with
+          | Tflat t => R t
+          | Arrow _ y => fun f g => forall x, interp_type_gen_rel_pointwise y (f x) (g x)
+          end.
+      End rel.
     End type.
     Section flat_type.
       Context (interp_base_type : base_type_code -> Type).