diff options
Diffstat (limited to 'src/Compilers')
-rw-r--r-- | src/Compilers/Named/ContextProperties.v | 6 | ||||
-rw-r--r-- | src/Compilers/Named/ContextProperties/Tactics.v | 3 |
2 files changed, 8 insertions, 1 deletions
diff --git a/src/Compilers/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v index 1db840753..9956f3b48 100644 --- a/src/Compilers/Named/ContextProperties.v +++ b/src/Compilers/Named/ContextProperties.v @@ -52,6 +52,12 @@ Section with_context. = find_Name_and_val t n N v (lookupb ctx n t). 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. + Proof using ContextOk. revert ctx; induction T; t. Qed. + Lemma find_Name_and_val_Some_None {var' var''} {t n T N} diff --git a/src/Compilers/Named/ContextProperties/Tactics.v b/src/Compilers/Named/ContextProperties/Tactics.v index 9616725d6..f438d5444 100644 --- a/src/Compilers/Named/ContextProperties/Tactics.v +++ b/src/Compilers/Named/ContextProperties/Tactics.v @@ -37,7 +37,8 @@ Ltac inversion_step := Ltac rewrite_lookupb_extendb_step := first [ rewrite lookupb_extendb_different by congruence | rewrite lookupb_extendb_same - | rewrite lookupb_extendb_wrong_type by assumption ]. + | rewrite lookupb_extendb_wrong_type by assumption + | rewrite lookupb_removeb by congruence ]. Ltac specializer_t_step := match goal with | _ => progress specialize_by_assumption |