Changeset 2510 for src/Clight/switchRemoval.ma

Timestamp:

Nov 30, 2012, 4:40:37 PM (7 years ago)

Author:

garnier

Message:

Some progress on the Cl -> Cm front

File:

• src/Clight/switchRemoval.ma (modified) (1 diff)

src/Clight/switchRemoval.ma

@@ -757 +757 @@
      <Hind <max_id_commutative >max_id_associative >(max_id_commutative b ?) @refl
 ] qed.
-
-(* Lookup functions in list environments (used to type local variables in functions) *)      
-let rec mem_assoc_env (i : ident) (l : list (ident×type)) on l : bool ≝
-match l with
-[ nil ⇒ false
-| cons hd tl ⇒
-  let 〈id, ty〉 ≝ hd in
-  match identifier_eq SymbolTag i id with
-  [ inl Hid_eq ⇒ true
-  | inr Hid_neq ⇒ mem_assoc_env i tl  
-  ]
-].
 
 (* --------------------------------------------------------------------------- *)