From ad997a5143d7e3cf81ef323b18fafc74f473549d Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 16 May 2017 22:41:43 -0400
Subject: Flip order of extendb, lookup arguments

This allows better Proper lemmas
---
 src/Compilers/CommonSubexpressionEliminationWf.v |  6 ++---
 src/Compilers/Named/AListContext.v               |  8 +++---
 src/Compilers/Named/CompileInterp.v              |  4 +--
 src/Compilers/Named/CompileWf.v                  |  4 +--
 src/Compilers/Named/Context.v                    | 32 ++++++++++++------------
 src/Compilers/Named/ContextDefinitions.v         | 16 ++++++------
 src/Compilers/Named/ContextOn.v                  |  6 ++---
 src/Compilers/Named/ContextProperties.v          | 20 +++++++--------
 src/Compilers/Named/EstablishLiveness.v          |  2 +-
 src/Compilers/Named/FMapContext.v                | 12 ++++-----
 src/Compilers/Named/InterpretToPHOAS.v           |  2 +-
 src/Compilers/Named/InterpretToPHOASWf.v         | 16 ++++++------
 src/Compilers/Named/RegisterAssign.v             |  4 +--
 src/Compilers/Named/RegisterAssignInterp.v       | 22 ++++++++--------
 src/Compilers/Named/Syntax.v                     |  2 +-
 src/Compilers/Named/Wf.v                         |  2 +-
 src/Compilers/Named/WfFromUnit.v                 |  4 +--
 17 files changed, 81 insertions(+), 81 deletions(-)

(limited to 'src')

diff --git a/src/Compilers/CommonSubexpressionEliminationWf.v b/src/Compilers/CommonSubexpressionEliminationWf.v
index 8d8a5d86f..76ed1fa96 100644
--- a/src/Compilers/CommonSubexpressionEliminationWf.v
+++ b/src/Compilers/CommonSubexpressionEliminationWf.v
@@ -83,10 +83,10 @@ Section symbolic.
           (m1 : @SymbolicExprContext (interp_flat_type var1))
           (m2 : @SymbolicExprContext (interp_flat_type var2))
           (Hlen : length m1 = length m2)
-          (Hm1m2None : forall t v, lookupb m1 v t = None <-> lookupb m2 v t = None)
+          (Hm1m2None : forall t v, lookupb t m1 v = None <-> lookupb t m2 v = None)
           (Hm1m2Some : forall t v sv1 sv2,
-              lookupb m1 v t = Some sv1
-              -> lookupb m2 v t = Some sv2
+              lookupb t m1 v = Some sv1
+              -> lookupb t m2 v = Some sv2
               -> forall k,
                   List.In k (flatten_binding_list
                                (t:=t)
diff --git a/src/Compilers/Named/AListContext.v b/src/Compilers/Named/AListContext.v
index 129229ee3..74b993af6 100644
--- a/src/Compilers/Named/AListContext.v
+++ b/src/Compilers/Named/AListContext.v
@@ -99,20 +99,20 @@ Section ctx.
 
   Definition AListContext : @Context base_type_code key var
     := {| ContextT := list (key * { t : _ & var t });
-          lookupb ctx n t
+          lookupb t ctx n
           := match find n ctx with
              | Some (existT t' v)
                => var_cast v
              | None => None
              end;
-          extendb ctx n t v
+          extendb t ctx n v
           := add n (existT _ t v) ctx;
-          removeb ctx n t
+          removeb t ctx n
           := remove n ctx;
           empty := nil |}.
 
   Lemma length_extendb (ctx : AListContext) k t v
-    : length (@extendb _ _ _ AListContext ctx k t v) = S (length ctx).
+    : length (@extendb _ _ _ AListContext t ctx k v) = S (length ctx).
   Proof. reflexivity. Qed.
 
   Lemma AListContextOk : @ContextOk base_type_code key var AListContext.
diff --git a/src/Compilers/Named/CompileInterp.v b/src/Compilers/Named/CompileInterp.v
index 32cc1e750..20a536ddc 100644
--- a/src/Compilers/Named/CompileInterp.v
+++ b/src/Compilers/Named/CompileInterp.v
@@ -49,7 +49,7 @@ Section language.
   Lemma interpf_ocompilef (ctx : Context) {t} (e : exprf t) e' (ls : list (option Name))
         G
         (Hwf : wff G e e')
-        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb ctx n t = Some x)
+        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x)
         v
         (H : ocompilef e ls = Some v)
         (Hls : oname_list_unique ls)
@@ -174,7 +174,7 @@ Section language.
   Lemma interpf_compilef (ctx : Context) {t} (e : exprf t) e' (ls : list Name)
         G
         (Hwf : wff G e e')
-        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb ctx n t = Some x)
+        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x)
         v
         (H : compilef e ls = Some v)
         (Hls : name_list_unique ls)
diff --git a/src/Compilers/Named/CompileWf.v b/src/Compilers/Named/CompileWf.v
index a741ad213..5b6b32bb5 100644
--- a/src/Compilers/Named/CompileWf.v
+++ b/src/Compilers/Named/CompileWf.v
@@ -48,7 +48,7 @@ Section language.
 
   Lemma wff_ocompilef (ctx : Context) G
         (HG : forall t n v,
-            List.In (existT _ t (n, v)%core) G -> lookupb ctx n t = Some v)
+            List.In (existT _ t (n, v)%core) G -> lookupb t ctx n = Some v)
         {t} (e : exprf t) e' (ls : list (option Name))
         (Hwf : wff G e e')
         v
@@ -205,7 +205,7 @@ Section language.
   Lemma wff_compilef (ctx : Context) {t} (e : exprf t) e' (ls : list Name)
         G
         (Hwf : wff G e e')
-        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb ctx n t = Some x)
+        (HG : forall t n x, List.In (existT _ t (n, x)%core) G -> lookupb t ctx n = Some x)
         v
         (H : compilef e ls = Some v)
         (Hls : name_list_unique ls)
diff --git a/src/Compilers/Named/Context.v b/src/Compilers/Named/Context.v
index ba0ad6feb..f63172de4 100644
--- a/src/Compilers/Named/Context.v
+++ b/src/Compilers/Named/Context.v
@@ -5,14 +5,14 @@ Require Import Crypto.Util.Notations.
 
 Record Context {base_type_code} (Name : Type) (var : base_type_code -> Type) :=
   { ContextT : Type;
-    lookupb : ContextT -> Name -> forall {t : base_type_code}, option (var t);
-    extendb : ContextT -> Name -> forall {t : base_type_code}, var t -> ContextT;
-    removeb : ContextT -> Name -> base_type_code -> ContextT;
+    lookupb : forall {t : base_type_code}, ContextT -> Name -> option (var t);
+    extendb : forall {t : base_type_code}, ContextT -> Name -> var t -> ContextT;
+    removeb : base_type_code -> ContextT -> Name -> ContextT;
     empty : ContextT }.
 Coercion ContextT : Context >-> Sortclass.
 Arguments ContextT {_ _ _ _}, {_ _ _} _.
-Arguments lookupb {_ _ _ _} _ _ {_}, {_ _ _ _} _ _ _.
-Arguments extendb {_ _ _ _} _ _ [_] _.
+Arguments lookupb {_ _ _ _ _} _ _, {_ _ _ _} _ _ _.
+Arguments extendb {_ _ _ _} [_] _ _ _.
 Arguments removeb {_ _ _ _} _ _ _.
 Arguments empty {_ _ _ _}.
 
@@ -24,31 +24,31 @@ Section language.
 
   Local Notation flat_type := (flat_type base_type_code).
 
-  Fixpoint extend (ctx : Context) {t : flat_type}
+  Fixpoint extend {t : flat_type} (ctx : Context)
            (n : interp_flat_type (fun _ => Name) t) (v : interp_flat_type var t)
     : Context
     := match t return interp_flat_type (fun _ => Name) t -> interp_flat_type var t -> Context with
        | Tbase t => fun n v => extendb ctx n v
        | Unit => fun _ _ => ctx
        | Prod A B => fun n v
-                     => let ctx := @extend ctx A (fst n) (fst v) in
-                        let ctx := @extend ctx B (snd n) (snd v) in
+                     => let ctx := @extend A ctx (fst n) (fst v) in
+                        let ctx := @extend B ctx (snd n) (snd v) in
                         ctx
        end n v.
 
-  Fixpoint remove (ctx : Context) {t : flat_type}
+  Fixpoint remove {t : flat_type} (ctx : Context)
            (n : interp_flat_type (fun _ => Name) t)
     : Context
     := match t return interp_flat_type (fun _ => Name) t -> Context with
-       | Tbase t => fun n => removeb ctx n t
+       | Tbase t => fun n => removeb t ctx n
        | Unit => fun _ => ctx
        | Prod A B => fun n
-                     => let ctx := @remove ctx A (fst n) in
-                        let ctx := @remove ctx B (snd n) in
+                     => let ctx := @remove A ctx (fst n) in
+                        let ctx := @remove B ctx (snd n) in
                         ctx
        end n.
 
-  Definition lookup (ctx : Context) {t}
+  Definition lookup {t} (ctx : Context)
     : interp_flat_type (fun _ => Name) t -> option (interp_flat_type var t)
     := smart_interp_flat_map
          (g := fun t => option (interp_flat_type var t))
@@ -60,6 +60,6 @@ Section language.
                          end).
 End language.
 
-Global Arguments extend {_ _ _ _} ctx {_} _ _.
-Global Arguments remove {_ _ _ _} ctx {_} _.
-Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _.
+Global Arguments extend {_ _ _ _} {_} ctx _ _.
+Global Arguments remove {_ _ _ _} {_} ctx _.
+Global Arguments lookup {_ _ _ _} {_} ctx _, {_ _ _ _} _ ctx _.
diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v
index f1a9b2741..79a3f2f1c 100644
--- a/src/Compilers/Named/ContextDefinitions.v
+++ b/src/Compilers/Named/ContextDefinitions.v
@@ -45,17 +45,17 @@ Section with_context.
 
   Class ContextOk :=
     { lookupb_extendb_same
-      : forall (ctx : Context) n t v, lookupb (extendb ctx n (t:=t) v) n t = Some v;
+      : forall (ctx : Context) n t v, lookupb t (extendb ctx n (t:=t) v) n = Some v;
       lookupb_extendb_different
-      : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb (extendb ctx n (t:=t) v) n' t'
-                                                       = lookupb ctx n' t';
+      : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb t' (extendb ctx n (t:=t) v) n'
+                                                       = lookupb t' ctx n';
       lookupb_extendb_wrong_type
-      : forall (ctx : Context) n t t' v, t <> t' -> lookupb (extendb ctx n (t:=t) v) n t' = None;
+      : forall (ctx : Context) n t t' v, t <> t' -> lookupb t' (extendb ctx n (t:=t) v) n = None;
       lookupb_removeb_different
-      : forall (ctx : Context) n n' t t', n <> n' -> lookupb (removeb ctx n t) n' t'
-                                                     = lookupb ctx n' t';
+      : forall (ctx : Context) n n' t t', n <> n' -> lookupb t' (removeb t ctx n) n'
+                                                     = lookupb t' ctx n';
       lookupb_removeb_same
-      : forall (ctx : Context) n t t', lookupb (removeb ctx n t) n t' = None;
+      : forall (ctx : Context) n t t', lookupb t' (removeb t ctx n) n = None;
       lookupb_empty
-      : forall n t, lookupb (@empty _ _ _ Context) n t = None }.
+      : forall n t, lookupb t (@empty _ _ _ Context) n = None }.
 End with_context.
diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v
index 4c02e26c7..3cd3fbc1a 100644
--- a/src/Compilers/Named/ContextOn.v
+++ b/src/Compilers/Named/ContextOn.v
@@ -10,9 +10,9 @@ Section language.
 
   Definition ContextOn (Ctx : Context Name1 var) : Context Name2 var
     := {| ContextT := Ctx;
-          lookupb ctx n t := lookupb ctx (f n) t;
-          extendb ctx n t v := extendb ctx (f n) v;
-          removeb ctx n t := removeb ctx (f n) t;
+          lookupb t ctx n := lookupb t ctx (f n);
+          extendb t ctx n v := extendb ctx (f n) v;
+          removeb t ctx n := removeb t ctx (f n);
           empty := empty |}.
 
   Lemma ContextOnOk {Ctx} (COk : ContextOk Ctx) : ContextOk (ContextOn Ctx).
diff --git a/src/Compilers/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v
index c7313d02d..782fc9a54 100644
--- a/src/Compilers/Named/ContextProperties.v
+++ b/src/Compilers/Named/ContextProperties.v
@@ -18,26 +18,26 @@ Section with_context.
 
   Lemma lookupb_eq_cast
     : forall (ctx : Context) n t t' (pf : t = t'),
-      lookupb ctx n t' = option_map (fun v => eq_rect _ var v _ pf) (lookupb ctx n t).
+      lookupb t' ctx n = option_map (fun v => eq_rect _ var v _ pf) (lookupb t ctx n).
   Proof.
     intros; subst; edestruct lookupb; reflexivity.
   Defined.
   Lemma lookupb_extendb_eq
     : forall (ctx : Context) n t t' (pf : t = t') v,
-      lookupb (extendb ctx n (t:=t) v) n t' = Some (eq_rect _ var v _ pf).
+      lookupb t' (extendb ctx n (t:=t) v) n = Some (eq_rect _ var v _ pf).
   Proof.
     intros; subst; apply lookupb_extendb_same; assumption.
   Defined.
 
   Lemma lookupb_extendb_full (ctx : Context) n n' t t' v
-    : lookupb (extendb ctx n (t:=t) v) n' t'
+    : lookupb t' (extendb ctx n (t:=t) v) n'
       = match dec (n = n'), dec (t = t') with
         | left _, left pf
           => Some (eq_rect _ var v _ pf)
         | left _, _
           => None
         | right _, _
-          => lookupb ctx n' t'
+          => lookupb t' ctx n'
         end.
   Proof using ContextOk.
     break_innermost_match; subst; simpl.
@@ -48,29 +48,29 @@ Section with_context.
 
   Lemma lookupb_extend (ctx : Context)
         T N t n v
-    : lookupb (extend ctx N (t:=T) v) n t
-      = find_Name_and_val t n N v (lookupb ctx n t).
+    : lookupb t (extend ctx N (t:=T) v) n
+      = find_Name_and_val t n N v (lookupb t ctx n).
   Proof using ContextOk. revert ctx; induction T; t. Qed.
 
   Lemma lookupb_remove (ctx : Context)
         T N t n
-    : lookupb (remove ctx N) n t
+    : lookupb t (remove ctx N) n
       = match @find_Name n T N with
         | Some _ => None
-        | None => lookupb ctx n t
+        | None => lookupb t ctx n
         end.
   Proof using ContextOk. revert ctx; induction T; t. Qed.
 
   Lemma lookupb_remove_not_in (ctx : Context)
         T N t n
         (H : @find_Name n T N = None)
-    : lookupb (remove ctx N) n t = lookupb ctx n t.
+    : lookupb t (remove ctx N) n = lookupb t ctx n.
   Proof using ContextOk. rewrite lookupb_remove, H; reflexivity. Qed.
 
   Lemma lookupb_remove_in (ctx : Context)
         T N t n
         (H : @find_Name n T N <> None)
-    : lookupb (remove ctx N) n t = None.
+    : lookupb t (remove ctx N) n = None.
   Proof using ContextOk. rewrite lookupb_remove; break_match; congruence. Qed.
 
   Lemma find_Name_and_val_Some_None
diff --git a/src/Compilers/Named/EstablishLiveness.v b/src/Compilers/Named/EstablishLiveness.v
index c2d6c273a..706327918 100644
--- a/src/Compilers/Named/EstablishLiveness.v
+++ b/src/Compilers/Named/EstablishLiveness.v
@@ -50,7 +50,7 @@ Section language.
       : list liveness
       := match e with
          | TT => prefix
-         | Var t' name => match lookup ctx (Tbase t') name with
+         | Var t' name => match lookup (Tbase t') ctx name with
                           | Some ls => ls
                           | _ => nil
                           end
diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v
index 04f22cc3b..02b0fd05c 100644
--- a/src/Compilers/Named/FMapContext.v
+++ b/src/Compilers/Named/FMapContext.v
@@ -25,15 +25,15 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E).
          end.
     Definition FMapContext : @Context base_type_code W.key var
       := {| ContextT := W.t { t : _ & var t };
-            lookupb ctx n t
+            lookupb t ctx n
             := match W.find n ctx with
                | Some (existT t' v)
                  => var_cast v
                | None => None
                end;
-            extendb ctx n t v
+            extendb t ctx n v
             := W.add n (existT _ t v) ctx;
-            removeb ctx n t
+            removeb t ctx n
             := W.remove n ctx;
             empty := W.empty _ |}.
     Lemma FMapContextOk : @ContextOk base_type_code W.key var FMapContext.
@@ -58,9 +58,9 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E).
 
     Definition FMapContext_nd : @Context base_type_code W.key (fun _ => var)
       := {| ContextT := W.t var;
-            lookupb ctx n t := W.find n ctx;
-            extendb ctx n t v := W.add n v ctx;
-            removeb ctx n t := W.remove n ctx;
+            lookupb t ctx n := W.find n ctx;
+            extendb t ctx n v := W.add n v ctx;
+            removeb t ctx n := W.remove n ctx;
             empty := W.empty _ |}.
   End ctx_nd.
 End FMapContextFun.
diff --git a/src/Compilers/Named/InterpretToPHOAS.v b/src/Compilers/Named/InterpretToPHOAS.v
index 1ccad6cad..4e74fc59a 100644
--- a/src/Compilers/Named/InterpretToPHOAS.v
+++ b/src/Compilers/Named/InterpretToPHOAS.v
@@ -27,7 +27,7 @@ Module Export Named.
         : @Syntax.exprf base_type_code op var t
         := match e in Named.exprf _ _ _ t return @Syntax.exprf base_type_code op var t with
            | Named.Var t' x
-             => match lookupb ctx x t' with
+             => match lookupb t' ctx x with
                 | Some v => Var v
                 | None => failf _
                 end
diff --git a/src/Compilers/Named/InterpretToPHOASWf.v b/src/Compilers/Named/InterpretToPHOASWf.v
index fd35ab12c..d2b3f18d3 100644
--- a/src/Compilers/Named/InterpretToPHOASWf.v
+++ b/src/Compilers/Named/InterpretToPHOASWf.v
@@ -54,9 +54,9 @@ Section language.
               | [ H : context[find_Name_and_val ?tdec ?ndec ?a ?b ?c ?d ?default] |- _ ]
                 => lazymatch default with None => fail | _ => idtac end;
                    rewrite (find_Name_and_val_split tdec ndec (default:=default)) in H
-              | [ H : forall n t, lookupb _ n t = None <-> lookupb _ n t = None |- context[lookupb _ _ = None] ]
+              | [ H : forall n t, lookupb _ n = None <-> lookupb _ n = None |- context[lookupb _ _ = None] ]
                 => rewrite H
-              | [ H : forall n t, lookupb _ n t = None |- context[lookupb _ _ = None] ]
+              | [ H : forall n t, lookupb _ n = None |- context[lookupb _ _ = None] ]
                 => rewrite H
               end ].
     Local Ltac t := repeat t_step.
@@ -68,11 +68,11 @@ Section language.
           (Hwf2 : prop_of_option (Named.wff ctx2 e))
           G
           (HG : forall n t v1 v2,
-              lookupb ctx1 n t = Some v1
-              -> lookupb ctx2 n t = Some v2
+              lookupb t ctx1 n = Some v1
+              -> lookupb t ctx2 n = Some v2
               -> List.In (existT _ t (v1, v2)%core) G)
           (Hctx1_ctx2 : forall n t,
-              lookupb ctx1 n t = None <-> lookupb ctx2 n t = None)
+              lookupb t ctx1 n = None <-> lookupb t ctx2 n = None)
       : wff G (interpf_to_phoas failb1 ctx1 e) (interpf_to_phoas failb2 ctx2 e).
     Proof using Context1Ok Context2Ok Name_dec base_type_code_dec.
       revert dependent G; revert dependent ctx1; revert dependent ctx2; induction e;
@@ -93,8 +93,8 @@ Section language.
           {t} (e : @Named.expr base_type_code op Name t)
           (Hwf1 : Named.wf ctx1 e)
           (Hwf2 : Named.wf ctx2 e)
-          (Hctx1 : forall n t, lookupb ctx1 n t = None)
-          (Hctx2 : forall n t, lookupb ctx2 n t = None)
+          (Hctx1 : forall n t, lookupb t ctx1 n = None)
+          (Hctx2 : forall n t, lookupb t ctx2 n = None)
       : wf (interp_to_phoas failb1 ctx1 e) (interp_to_phoas failb2 ctx2 e).
     Proof using Context1Ok Context2Ok Name_dec base_type_code_dec.
       constructor; intros.
@@ -119,7 +119,7 @@ Section language.
     Lemma Wf_InterpToPHOAS_gen
           {ctx : forall var, Context var}
           {t} (e : @Named.expr base_type_code op Name t)
-          (Hctx : forall var n t, lookupb (ctx var) n t = None)
+          (Hctx : forall var n t, lookupb t (ctx var) n = None)
           (Hwf : forall var, Named.wf (ctx var) e)
       : Wf (InterpToPHOAS_gen failb ctx e).
     Proof using ContextOk Name_dec base_type_code_dec.
diff --git a/src/Compilers/Named/RegisterAssign.v b/src/Compilers/Named/RegisterAssign.v
index 869d959ec..0b6c9b7b9 100644
--- a/src/Compilers/Named/RegisterAssign.v
+++ b/src/Compilers/Named/RegisterAssign.v
@@ -34,9 +34,9 @@ Section language.
       : option (exprf OutName t)
       := match e in Named.exprf _ _ _ t return option (exprf _ t) with
          | TT => Some TT
-         | Var t' name => match lookupb ctxi name t' with
+         | Var t' name => match lookupb t' ctxi name with
                           | Some new_name
-                            => match lookupb ctxr new_name t' with
+                            => match lookupb t' ctxr new_name with
                                | Some name'
                                  => if InName_beq name name'
                                     then Some (Var new_name)
diff --git a/src/Compilers/Named/RegisterAssignInterp.v b/src/Compilers/Named/RegisterAssignInterp.v
index bcf276517..be0e9cace 100644
--- a/src/Compilers/Named/RegisterAssignInterp.v
+++ b/src/Compilers/Named/RegisterAssignInterp.v
@@ -80,9 +80,9 @@ Section language.
   Proof using Type. t_find T. Qed.
 
   Lemma lookupb_extend_helper {ctxi : InContext} {ctxr : ReverseContext} {t T NI NO n_in n_out}
-        (H0 : lookupb (extend (t:=T) ctxi NI NO) n_in t = Some n_out)
-        (H1 : lookupb (extend (t:=T) ctxr NO NI) n_out t = Some n_in)
-    : ((lookupb ctxi n_in t = Some n_out /\ lookupb ctxr n_out t = Some n_in)
+        (H0 : lookupb t (extend (t:=T) ctxi NI NO) n_in = Some n_out)
+        (H1 : lookupb t (extend (t:=T) ctxr NO NI) n_out = Some n_in)
+    : ((lookupb t ctxi n_in = Some n_out /\ lookupb t ctxr n_out = Some n_in)
        /\ (find_Name _ n_in NI = None /\ find_Name _ n_out NO = None))
       \/ (find_Name_and_val _ _ t n_in NI NO None = Some n_out
           /\ find_Name_and_val _ _ t n_out NO NI None = Some n_in).
@@ -186,10 +186,10 @@ Section language.
         eout
         v1 v2
     : (forall t (n_in : InName) (n_out : OutName) v1 v2,
-          lookupb ctxi n_in t = Some n_out
-          -> lookupb ctxr n_out t = Some n_in
-          -> lookupb ctxi_interp n_in t = Some v1
-          -> lookupb ctxr_interp n_out t = Some v2
+          lookupb t ctxi n_in = Some n_out
+          -> lookupb t ctxr n_out = Some n_in
+          -> lookupb t ctxi_interp n_in = Some v1
+          -> lookupb t ctxr_interp n_out = Some v2
           -> v1 = v2)
       -> @register_reassignf ctxi ctxr t e new_names = Some eout
       -> interpf (interp_op:=interp_op) (ctx:=ctxr_interp) eout = Some v1
@@ -207,10 +207,10 @@ Section language.
         eout
         v1 v2 x
     : (forall t (n_in : InName) (n_out : OutName) v1 v2,
-          lookupb ctxi n_in t = Some n_out
-          -> lookupb ctxr n_out t = Some n_in
-          -> lookupb ctxi_interp n_in t = Some v1
-          -> lookupb ctxr_interp n_out t = Some v2
+          lookupb t ctxi n_in = Some n_out
+          -> lookupb t ctxr n_out = Some n_in
+          -> lookupb t ctxi_interp n_in = Some v1
+          -> lookupb t ctxr_interp n_out = Some v2
           -> v1 = v2)
       -> @register_reassign ctxi ctxr t e new_names = Some eout
       -> interp (interp_op:=interp_op) (ctx:=ctxr_interp) eout x = Some v1
diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v
index 453e37de9..34ba1f48f 100644
--- a/src/Compilers/Named/Syntax.v
+++ b/src/Compilers/Named/Syntax.v
@@ -44,7 +44,7 @@ Module Export Named.
                (ctx : Context) {t} (e : exprf t)
         : option (interp_flat_type t)
         := match e in exprf t return option (interp_flat_type t) with
-           | Var t' x => lookupb ctx x t'
+           | Var t' x => lookupb t' ctx x
            | TT => Some tt
            | Pair _ ex _ ey
              => match @interpf ctx _ ex, @interpf ctx _ ey with
diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v
index 736d0bd81..79f620edb 100644
--- a/src/Compilers/Named/Wf.v
+++ b/src/Compilers/Named/Wf.v
@@ -18,7 +18,7 @@ Module Export Named.
         Fixpoint wff_gen (ctx : Context) {t} (e : @exprf base_type_code op Name t) : option pointed_Prop
           := match e with
              | TT => Some trivial
-             | Var t n => match lookupb ctx n t return bool with
+             | Var t n => match lookupb t ctx n return bool with
                           | Some _ => true
                           | None => false
                           end
diff --git a/src/Compilers/Named/WfFromUnit.v b/src/Compilers/Named/WfFromUnit.v
index c6b28f824..e00a79274 100644
--- a/src/Compilers/Named/WfFromUnit.v
+++ b/src/Compilers/Named/WfFromUnit.v
@@ -50,7 +50,7 @@ Section language.
     Lemma wff_from_unit
           (vctx : vContext)
           (uctx : uContext)
-          (Hctx : forall t n, lookupb vctx n t = None <-> lookupb uctx n t = None)
+          (Hctx : forall t n, lookupb t vctx n = None <-> lookupb t uctx n = None)
           {t} (e : @exprf base_type_code op Name t)
       : wff_unit uctx e = Some trivial -> prop_of_option (wff vctx e).
     Proof using Name_dec base_type_code_dec uContextOk vContextOk.
@@ -60,7 +60,7 @@ Section language.
     Lemma wf_from_unit
           (vctx : vContext)
           (uctx : uContext)
-          (Hctx : forall t n, lookupb vctx n t = None <-> lookupb uctx n t = None)
+          (Hctx : forall t n, lookupb t vctx n = None <-> lookupb t uctx n = None)
           {t} (e : @expr base_type_code op Name t)
       : wf_unit uctx e = Some trivial -> wf vctx e.
     Proof using Name_dec base_type_code_dec uContextOk vContextOk.
-- 
cgit v1.2.3