diff options
Diffstat (limited to 'src/Compilers/Named/ContextDefinitions.v')
| -rw-r--r-- | src/Compilers/Named/ContextDefinitions.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v index 79a3f2f1c..010cf1fca 100644 --- a/src/Compilers/Named/ContextDefinitions.v +++ b/src/Compilers/Named/ContextDefinitions.v @@ -58,4 +58,7 @@ Section with_context. : 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 }. + + Definition context_equiv (a b : Context) + := forall n t, lookupb t a n = lookupb t b n. End with_context. |