Stronger contexts

4 files changed, 11 insertions, 4 deletions

diff --git a/src/Compilers/Named/AListContext.v b/src/Compilers/Named/AListContext.v
index 74b993af6..ffc8355ee 100644
--- a/src/Compilers/Named/AListContext.v
+++ b/src/Compilers/Named/AListContext.v
@@ -136,6 +136,8 @@ Section ctx.
                    | rewrite key_lb in * by reflexivity
                    | rewrite base_type_code_lb in * by reflexivity
                    | rewrite concat_pV
-                   | congruence ].
+                   | congruence
+                   | break_innermost_match_hyps_step
+                   | progress unfold var_cast in * ].
   Qed.
 End ctx.
diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v
index 010cf1fca..1b57e5b51 100644
--- a/src/Compilers/Named/ContextDefinitions.v
+++ b/src/Compilers/Named/ContextDefinitions.v
@@ -57,7 +57,10 @@ Section with_context.
       lookupb_removeb_same
       : forall (ctx : Context) n t t', lookupb t' (removeb t ctx n) n = None;
       lookupb_empty
-      : forall n t, lookupb t (@empty _ _ _ Context) n = None }.
+      : forall n t, lookupb t (@empty _ _ _ Context) n = None;
+
+      lookupb_unique_type
+      : forall (ctx : Context) n t t', lookupb t' ctx n <> None -> lookupb t ctx n <> None -> t = t' }.
 
   Definition context_equiv (a b : Context)
     := forall n t, lookupb t a n = lookupb t b n.
diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v
index 3cd3fbc1a..17d8690fc 100644
--- a/src/Compilers/Named/ContextOn.v
+++ b/src/Compilers/Named/ContextOn.v
@@ -17,7 +17,7 @@ Section language.
 
   Lemma ContextOnOk {Ctx} (COk : ContextOk Ctx) : ContextOk (ContextOn Ctx).
   Proof.
-    split; intros; try apply COk; auto.
+    unfold ContextOn in *; split; intros; try eapply COk; eauto.
   Qed.
 End language.
 
diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v
index 02b0fd05c..b69d78d09 100644
--- a/src/Compilers/Named/FMapContext.v
+++ b/src/Compilers/Named/FMapContext.v
@@ -49,7 +49,9 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E).
                      | progress break_innermost_match_step
                      | rewrite concat_pV
                      | congruence
-                     | rewrite base_type_code_lb in * by reflexivity ].
+                     | rewrite base_type_code_lb in * by reflexivity
+                     | break_innermost_match_hyps_step
+                     | progress unfold var_cast in * ].
     Qed.
   End ctx.