Changeset 1465 for src/common

Timestamp:

Oct 26, 2011, 2:07:41 PM (9 years ago)

Author:

sacerdot

Message:

Dead code removed.

File:

• src/common/AST.ma (modified) (1 diff)

src/common/AST.ma

@@ -664 +664 @@
       bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
   ].
-
-(* TODO: merge in comparison definitions from Integers.ma. *)
-inductive Compare: Type[0] ≝
-  Compare_Equal: Compare
-| Compare_NotEqual: Compare
-| Compare_Less: Compare
-| Compare_Greater: Compare
-| Compare_LessEqual: Compare
-| Compare_GreaterEqual: Compare.
-
-inductive op1: Type[0] ≝
-  | op_cast: nat → signedness → nat → op1
-  | op_neg_int: op1          (**r integer opposite *)
-  | op_not_bool: op1         (**r boolean negation  *)
-  | op_not_int: op1          (**r bitwise complement  *)
-  | op_id: op1               (**r identity *)
-  | op_ptr_of_int: op1       (**r int to pointer *)
-  | op_int_of_ptr: op1.      (**r pointer to int *)
-
-inductive op2: Type[0] ≝
-  | op_add: op2         (**r integer addition *)
-  | op_sub: op2         (**r integer subtraction *)
-  | op_mul: op2         (**r integer multiplication *)
-  | op_div: op2         (**r integer signed division *)
-  | op_divu: op2        (**r integer unsigned division *)
-  | op_mod: op2         (**r integer signed modulus *)
-  | op_modu: op2        (**r integer unsigned modulus *)
-  | op_and: op2         (**r bitwise ``and'' *)
-  | op_or: op2          (**r bitwise ``or'' *)
-  | op_xor: op2         (**r bitwise ``xor'' *)
-  | op_shl: op2         (**r left shift *)
-  | op_shr: op2         (**r right signed shift *)
-  | op_shru: op2        (**r right unsigned shift *)
-  | op_cmp: Compare → op2   (**r integer signed comparison *)
-  | op_cmpu: Compare → op2  (**r integer unsigned comparison *)
-  | op_addp: op2        (**r addition for a pointer and an integer *)
-  | op_subp: op2        (**r substraction for a pointer and a integer *)
-  | op_subpp: op2
-  | op_cmpp: Compare → op2. (**r pointer comparaison *)