diff options
Diffstat (limited to 'src/Compilers/Named/AListContext.v')
-rw-r--r-- | src/Compilers/Named/AListContext.v | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/Compilers/Named/AListContext.v b/src/Compilers/Named/AListContext.v index 129229ee3..74b993af6 100644 --- a/src/Compilers/Named/AListContext.v +++ b/src/Compilers/Named/AListContext.v @@ -99,20 +99,20 @@ Section ctx. Definition AListContext : @Context base_type_code key var := {| ContextT := list (key * { t : _ & var t }); - lookupb ctx n t + lookupb t ctx n := match find n ctx with | Some (existT t' v) => var_cast v | None => None end; - extendb ctx n t v + extendb t ctx n v := add n (existT _ t v) ctx; - removeb ctx n t + removeb t ctx n := remove n ctx; empty := nil |}. Lemma length_extendb (ctx : AListContext) k t v - : length (@extendb _ _ _ AListContext ctx k t v) = S (length ctx). + : length (@extendb _ _ _ AListContext t ctx k v) = S (length ctx). Proof. reflexivity. Qed. Lemma AListContextOk : @ContextOk base_type_code key var AListContext. |