diff options
Diffstat (limited to 'src/Compilers/Named/ContextOn.v')
| -rw-r--r-- | src/Compilers/Named/ContextOn.v | 6 |
1 files changed, 3 insertions, 3 deletions
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). |