diff options
| author |  Jason Gross <jgross@mit.edu> | 2017-04-13 15:55:58 -0400 |
|---|---|---|
| committer | Jason Gross <jgross@mit.edu> | 2017-04-13 15:55:58 -0400 |
| commit | 7ae1f1d66c5d0cc5b7236162c7a14698a2c0e6c2 (patch) | |
| tree | 4effd0847db1b58cfb66cdb01e1e7c0d62941abd /src/Compilers/Named/FMapContext.v | |
| parent | e860b3d92634bfb11d54b96effc05cb2aa9dba41 (diff) | |
Add lookupb_removeb_same
Diffstat (limited to 'src/Compilers/Named/FMapContext.v')
| -rw-r--r-- | src/Compilers/Named/FMapContext.v | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v index 5519881c8..04f22cc3b 100644 --- a/src/Compilers/Named/FMapContext.v +++ b/src/Compilers/Named/FMapContext.v @@ -43,7 +43,7 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E). | progress simpl in * | progress intros | rewrite add_eq_o by reflexivity - | progress rewrite ?add_neq_o, ?remove_neq_o in * by intuition + | progress rewrite ?add_neq_o, ?remove_neq_o, ?remove_eq_o in * by intuition | progress rewrite empty_o in * | progress unfold var_cast | progress break_innermost_match_step |