Add [f] to things that use [exprf] or [flat_type]

13 files changed, 57 insertions, 57 deletions

diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v
index 927e7a168..8de6e7a2f 100644
--- a/src/Reflection/CountLets.v
+++ b/src/Reflection/CountLets.v
@@ -33,7 +33,7 @@ Section language.
       Fixpoint count_lets_genf {t} (e : exprf t) : nat
         := match e with
            | LetIn tx _ _ eC
-             => count_type_let tx + @count_lets_genf _ (eC (SmartVal var mkVar tx))
+             => count_type_let tx + @count_lets_genf _ (eC (SmartValf var mkVar tx))
            | _ => 0
            end.
       Fixpoint count_lets_gen {t} (e : expr t) : nat
diff --git a/src/Reflection/FilterLive.v b/src/Reflection/FilterLive.v
index 3c1c3c8f7..446f9195c 100644
--- a/src/Reflection/FilterLive.v
+++ b/src/Reflection/FilterLive.v
@@ -50,7 +50,7 @@ Section language.
             | Some n =>
               @filter_live_namesf
                 (prefix ++ repeat dead_name (count_pairs tx))%list remaining' _
-                (eC (SmartVal (fun _ => list Name) (fun _ => namesx ++ names_to_list n)%list _))
+                (eC (SmartValf (fun _ => list Name) (fun _ => namesx ++ names_to_list n)%list _))
             | None => nil
             end
        | Pair _ ex _ ey => merge_name_lists (@filter_live_namesf prefix remaining _ ex)
diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v
index bfb3794c9..a42df2b68 100644
--- a/src/Reflection/Inline.v
+++ b/src/Reflection/Inline.v
@@ -33,12 +33,12 @@ Section language.
            => match postprocess _ (@inline_const_genf _ ex) in inline_directive t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with
               | default_inline _ ex
                 => match ex in Syntax.exprf _ _ _ t' return (interp_flat_type _ t' -> @exprf var tC) -> @exprf var tC with
-                   | Const _ x => fun eC => eC (SmartConst (op:=op) (var:=var) x)
+                   | Const _ x => fun eC => eC (SmartConstf (op:=op) (var:=var) x)
                    | Var _ x => fun eC => eC (Var x)
-                   | ex => fun eC => LetIn ex (fun x => eC (SmartVarVar x))
+                   | ex => fun eC => LetIn ex (fun x => eC (SmartVarVarf x))
                    end
               | no_inline _ ex
-                => fun eC => LetIn ex (fun x => eC (SmartVarVar x))
+                => fun eC => LetIn ex (fun x => eC (SmartVarVarf x))
               | inline _ ex => fun eC => eC ex
               end (fun x => @inline_const_genf _ (eC x))
          | Var _ x => x
diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
index 83751e4f2..27811914c 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Reflection/InlineInterp.v
@@ -25,8 +25,8 @@ Section language.
   Local Notation wff := (@wff base_type_code interp_base_type op).
   Local Notation wf := (@wf base_type_code interp_base_type op).
 
-  Local Hint Extern 1 => eapply interpf_SmartConst.
-  Local Hint Extern 1 => eapply interpf_SmartVarVar.
+  Local Hint Extern 1 => eapply interpf_SmartConstf.
+  Local Hint Extern 1 => eapply interpf_SmartVarVarf.
 
   Local Ltac t_fin :=
     repeat match goal with
diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
index 781643a8a..dd0fb08a3 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Reflection/InlineWf.v
@@ -32,8 +32,8 @@ Section language.
     Local Hint Constructors Syntax.wff.
     Local Hint Extern 1 => progress unfold List.In in *.
     Local Hint Resolve wff_in_impl_Proper.
-    Local Hint Resolve wff_SmartVar.
-    Local Hint Resolve wff_SmartConst.
+    Local Hint Resolve wff_SmartVarf.
+    Local Hint Resolve wff_SmartConstf.
 
     Local Ltac t_fin :=
       repeat first [ intro
@@ -42,9 +42,9 @@ Section language.
                    | tauto
                    | progress subst
                    | solve [ auto with nocore
-                           | eapply (@wff_SmartVarVar _ _ _ _ _ _ _ (_ * _)); auto
-                           | eapply wff_SmartConst; eauto with nocore
-                           | eapply wff_SmartVarVar; eauto with nocore ]
+                           | eapply (@wff_SmartVarVarf _ _ _ _ _ _ _ (_ * _)); auto
+                           | eapply wff_SmartConstf; eauto with nocore
+                           | eapply wff_SmartVarVarf; eauto with nocore ]
                    | progress simpl in *
                    | constructor
                    | solve [ eauto ] ].
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v
index 7a89a22d3..dd9cab21d 100644
--- a/src/Reflection/InputSyntax.v
+++ b/src/Reflection/InputSyntax.v
@@ -70,7 +70,7 @@ Section language.
       Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code interp_base_type op var t
         := match e in exprf t return @Syntax.exprf _ _ _ _ t with
            | Const _ x => Syntax.Const x
-           | Var _ x => Syntax.SmartVar x
+           | Var _ x => Syntax.SmartVarf x
            | Op _ _ op args => Syntax.Op op (@compilef _ args)
            | LetIn _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun x => @compilef _ (eC x))
            | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey)
@@ -98,7 +98,7 @@ Section language.
                  | _ => reflexivity
                  | _ => progress unfold LetIn.Let_In
                  | _ => progress simpl in *
-                 | _ => rewrite interpf_SmartVar
+                 | _ => rewrite interpf_SmartVarf
                  | _ => rewrite <- surjective_pairing
                  | _ => progress rewrite_hyp *
                  | [ |- context[let (x, y) := ?v in _] ]
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index 86e8190ea..880256f1d 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -16,10 +16,10 @@ Section language.
   Let interp_flat_type := interp_flat_type interp_base_type.
   Context (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
 
-  Lemma interpf_SmartVar t v
-    : Syntax.interpf interp_op (SmartVar (t:=t) v) = v.
+  Lemma interpf_SmartVarf t v
+    : Syntax.interpf interp_op (SmartVarf (t:=t) v) = v.
   Proof.
-    unfold SmartVar; induction t;
+    unfold SmartVarf; induction t;
       repeat match goal with
              | _ => reflexivity
              | _ => progress simpl in *
@@ -28,11 +28,11 @@ Section language.
              end.
   Qed.
 
-  Lemma interpf_SmartConst {t t'} v x x'
+  Lemma interpf_SmartConstf {t t'} v x x'
         (Hin : List.In
                  (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
                          t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartConst v) v))
+                 (flatten_binding_list (t := t') base_type_code (SmartConstf v) v))
     : interpf interp_op x = x'.
   Proof.
     clear -Hin.
@@ -42,11 +42,11 @@ Section language.
       intuition (inversion_sigma; inversion_prod; subst; eauto). }
   Qed.
 
-  Lemma interpf_SmartVarVar {t t'} v x x'
+  Lemma interpf_SmartVarVarf {t t'} v x x'
         (Hin : List.In
                  (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
                          t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v) v))
+                 (flatten_binding_list (t := t') base_type_code (SmartVarVarf v) v))
     : interpf interp_op x = x'.
   Proof.
     clear -Hin.
@@ -56,14 +56,14 @@ Section language.
       intuition (inversion_sigma; inversion_prod; subst; eauto). }
   Qed.
 
-  Lemma interpf_SmartVarVar_eq {t t'} v v' x x'
+  Lemma interpf_SmartVarVarf_eq {t t'} v v' x x'
         (Heq : v = v')
         (Hin : List.In
                  (existT (fun t : base_type_code => (exprf base_type_code interp_base_type op (Syntax.Tbase t) * interp_base_type t)%type)
                          t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartVarVar v') v))
+                 (flatten_binding_list (t := t') base_type_code (SmartVarVarf v') v))
     : interpf interp_op x = x'.
   Proof.
-    subst; eapply interpf_SmartVarVar; eassumption.
+    subst; eapply interpf_SmartVarVarf; eassumption.
   Qed.
 End language.
diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v
index 8dafbdc11..810d9115b 100644
--- a/src/Reflection/Linearize.v
+++ b/src/Reflection/Linearize.v
@@ -53,11 +53,11 @@ Section language.
          | Const _ x => Const x
          | Var _ x => Var x
          | Op _ _ op args
-           => under_letsf (@linearizef _ args) (fun args => LetIn (Op op (SmartVar args)) SmartVar)
+           => under_letsf (@linearizef _ args) (fun args => LetIn (Op op (SmartVarf args)) SmartVarf)
          | Pair A ex B ey
            => under_letsf (@linearizef _ ex) (fun x =>
               under_letsf (@linearizef _ ey) (fun y =>
-              SmartVar (t:=Prod A B) (x, y)))
+              SmartVarf (t:=Prod A B) (x, y)))
          end.
 
     Fixpoint linearize {t} (e : expr t) : expr t
diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v
index 35caa016c..3ee3960d5 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Reflection/LinearizeInterp.v
@@ -25,8 +25,8 @@ Section language.
   Local Notation wff := (@wff base_type_code interp_base_type op).
   Local Notation wf := (@wf base_type_code interp_base_type op).
 
-  Local Hint Extern 1 => eapply interpf_SmartConst.
-  Local Hint Extern 1 => eapply interpf_SmartVarVar.
+  Local Hint Extern 1 => eapply interpf_SmartConstf.
+  Local Hint Extern 1 => eapply interpf_SmartVarVarf.
 
   Local Ltac t_fin :=
     repeat match goal with
@@ -70,7 +70,7 @@ Section language.
   Proof.
     clear.
     induction e;
-      repeat first [ progress rewrite ?interpf_under_letsf, ?interpf_SmartVar
+      repeat first [ progress rewrite ?interpf_under_letsf, ?interpf_SmartVarf
                    | progress simpl
                    | t_fin ].
   Qed.
diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v
index 8a7ebb7af..36c9efecb 100644
--- a/src/Reflection/LinearizeWf.v
+++ b/src/Reflection/LinearizeWf.v
@@ -161,7 +161,7 @@ Section language.
     Local Hint Constructors or.
     Local Hint Extern 1 => progress unfold List.In in *.
     Local Hint Resolve wff_in_impl_Proper.
-    Local Hint Resolve wff_SmartVar.
+    Local Hint Resolve wff_SmartVarf.
 
     Lemma wff_linearizef G {t} e1 e2
       : @wff var1 var2 G t e1 e2
diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v
index b9d283013..b2be2d19b 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -62,7 +62,7 @@ Section language.
          | LetIn tx n ex _ eC
            => let lx := @compute_livenessf ctx _ ex prefix in
               let lx := merge_liveness lx (prefix ++ repeat live (count_pairs tx)) in
-              let ctx := extend ctx n (SmartVal _ (fun _ => lx) tx) in
+              let ctx := extend ctx n (SmartValf _ (fun _ => lx) tx) in
               @compute_livenessf ctx _ eC (prefix ++ repeat dead (count_pairs tx))
          | Pair _ ex _ ey
            => merge_liveness (@compute_livenessf ctx _ ex prefix)
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 4e650203c..30e5b6270 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -167,27 +167,27 @@ Section language.
            | Arrow A B => fun v => abs _ _
                                        (fun x => @smart_interp_map f g h h' pair abs B (v (h' _ x)))
            end.
-      Fixpoint SmartVal {T} (val : forall t : base_type_code, T t) t : interp_flat_type_gen T t
+      Fixpoint SmartValf {T} (val : forall t : base_type_code, T t) t : interp_flat_type_gen T t
         := match t return interp_flat_type_gen T t with
            | Tbase _ => val _
-           | Prod A B => (@SmartVal T val A, @SmartVal T val B)
+           | Prod A B => (@SmartValf T val A, @SmartValf T val B)
            end.
 
       (** [SmartVar] is like [Var], except that it inserts
           pair-projections and [Pair] as necessary to handle
           [flat_type], and not just [base_type_code] *)
-      Definition SmartVar {t} : interp_flat_type_gen var t -> exprf t
+      Definition SmartVarf {t} : interp_flat_type_gen var t -> exprf t
         := @smart_interp_flat_map var exprf (fun t => Var) (fun A B x y => Pair x y) t.
-      Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) {t}
+      Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t}
         : interp_flat_type_gen var t -> interp_flat_type_gen var' t
         := @smart_interp_flat_map var (interp_flat_type_gen var') f (fun A B x y => pair x y) t.
-      Definition SmartVarMapT {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t}
+      Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t}
         : interp_type_gen (interp_flat_type_gen var) t -> interp_type_gen (interp_flat_type_gen var') t
         := @smart_interp_map var (interp_type_gen (interp_flat_type_gen var')) f f' (fun A B x y => pair x y) (fun A B f x => f x) t.
-      Definition SmartVarVar {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t
-        := SmartVarMap (fun t => Var).
-      Definition SmartConst {t} : interp_flat_type t -> interp_flat_type_gen exprf t
-        := SmartVarMap (fun t => Const (t:=t)).
+      Definition SmartVarVarf {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t
+        := SmartVarfMap (fun t => Var).
+      Definition SmartConstf {t} : interp_flat_type t -> interp_flat_type_gen exprf t
+        := SmartVarfMap (fun t => Const (t:=t)).
     End expr.
 
     Definition Expr (t : type) := forall var, @expr var t.
@@ -289,12 +289,12 @@ Ltac admit_Wf := apply Wf_admitted.
 
 Global Arguments Const {_ _ _ _ _} _.
 Global Arguments Var {_ _ _ _ _} _.
-Global Arguments SmartVar {_ _ _ _ _} _.
-Global Arguments SmartVal {_} T _ t.
-Global Arguments SmartVarVar {_ _ _ _ _} _.
-Global Arguments SmartVarMap {_ _ _} _ {_} _.
-Global Arguments SmartVarMapT {_ _ _} _ _ {_} _.
-Global Arguments SmartConst {_ _ _ _ _} _.
+Global Arguments SmartVarf {_ _ _ _ _} _.
+Global Arguments SmartValf {_} T _ t.
+Global Arguments SmartVarVarf {_ _ _ _ _} _.
+Global Arguments SmartVarfMap {_ _ _} _ {_} _.
+Global Arguments SmartVarMap {_ _ _} _ _ {_} _.
+Global Arguments SmartConstf {_ _ _ _ _} _.
 Global Arguments Op {_ _ _ _ _ _} _ _.
 Global Arguments LetIn {_ _ _ _ _} _ {_} _.
 Global Arguments Pair {_ _ _ _ _} _ {_} _.
diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v
index 1e8eed632..acc72cc76 100644
--- a/src/Reflection/WfProofs.v
+++ b/src/Reflection/WfProofs.v
@@ -70,14 +70,14 @@ Section language.
     Local Hint Extern 1 => progress unfold List.In in *.
     Local Hint Resolve wff_in_impl_Proper.
 
-    Lemma wff_SmartVar {t} x1 x2
-      : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVar x1) (SmartVar x2).
+    Lemma wff_SmartVarf {t} x1 x2
+      : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVarf x1) (SmartVarf x2).
     Proof.
-      unfold SmartVar.
+      unfold SmartVarf.
       induction t; simpl; constructor; eauto.
     Qed.
 
-    Local Hint Resolve wff_SmartVar.
+    Local Hint Resolve wff_SmartVarf.
 
     Lemma wff_Const_eta G {A B} v1 v2
       : @wff var1 var2 G (Prod A B) (Const v1) (Const v2)
@@ -100,30 +100,30 @@ Section language.
 
     Local Hint Resolve wff_Const_eta_fst wff_Const_eta_snd.
 
-    Lemma wff_SmartConst G {t t'} v1 v2 x1 x2
+    Lemma wff_SmartConstf G {t t'} v1 v2 x1 x2
           (Hin : List.In (existT (fun t : base_type_code => (@exprf var1 t * @exprf var2 t)%type) t (x1, x2))
-                         (flatten_binding_list base_type_code (SmartConst v1) (SmartConst v2)))
+                         (flatten_binding_list base_type_code (SmartConstf v1) (SmartConstf v2)))
           (Hwf : @wff var1 var2 G t' (Const v1) (Const v2))
       : @wff var1 var2 G t x1 x2.
     Proof.
       induction t'. simpl in *.
       { intuition (inversion_sigma; inversion_prod; subst; eauto). }
-      { unfold SmartConst in *; simpl in *.
+      { unfold SmartConstf in *; simpl in *.
         apply List.in_app_iff in Hin.
         intuition (inversion_sigma; inversion_prod; subst; eauto). }
     Qed.
 
-    Local Hint Resolve wff_SmartConst.
+    Local Hint Resolve wff_SmartConstf.
 
-    Lemma wff_SmartVarVar G {t t'} v1 v2 x1 x2
+    Lemma wff_SmartVarVarf G {t t'} v1 v2 x1 x2
           (Hin : List.In (existT (fun t : base_type_code => (exprf t * exprf t)%type) t (x1, x2))
-                          (flatten_binding_list base_type_code (SmartVarVar v1) (SmartVarVar v2)))
+                          (flatten_binding_list base_type_code (SmartVarVarf v1) (SmartVarVarf v2)))
       : @wff var1 var2 (flatten_binding_list base_type_code (t:=t') v1 v2 ++ G) t x1 x2.
     Proof.
       revert dependent G; induction t'; intros. simpl in *.
       { intuition (inversion_sigma; inversion_prod; subst; simpl; eauto).
         constructor; eauto. }
-      { unfold SmartVarVar in *; simpl in *.
+      { unfold SmartVarVarf in *; simpl in *.
         apply List.in_app_iff in Hin.
         intuition (inversion_sigma; inversion_prod; subst; eauto).
         { rewrite <- !List.app_assoc; eauto. } }