Commit 48b8404b authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove some axioms from the generated Coq files.

This is getting tedious. There should be a way to drop the content of a
whole theory.
parent 3fb1cb52
......@@ -85,6 +85,8 @@ theory int.Abs
syntax function abs "(Zabs %1)"
remove prop Abs_pos
end
theory int.MinMax
......@@ -101,6 +103,12 @@ theory int.EuclideanDivision
syntax function div "(Zdiv %1 %2)"
syntax function mod "(Zmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Mod_1
remove prop Div_1
end
theory int.ComputerDivision
......@@ -110,6 +118,21 @@ theory int.ComputerDivision
syntax function div "(ZOdiv %1 %2)"
syntax function mod "(ZOmod %1 %2)"
remove prop Div_mod
remove prop Div_bound
remove prop Mod_bound
remove prop Div_sign_pos
remove prop Div_sign_neg
remove prop Mod_sign_pos
remove prop Mod_sign_neg
remove prop Rounds_toward_zero
remove prop Div_1
remove prop Mod_1
remove prop Div_inf
remove prop Mod_inf
remove prop Div_mult
remove prop Mod_mult
end
......@@ -146,6 +169,9 @@ theory real.Real
remove prop Trans
remove prop Antisymm
remove prop Total
remove prop assoc_mul_div
remove prop assoc_div_mul
remove prop assoc_div_div
end
......@@ -170,6 +196,7 @@ theory real.Abs
syntax function abs "(Rabs %1)"
remove prop Abs_le
remove prop Abs_pos
end
......@@ -178,6 +205,13 @@ theory real.FromInt
syntax function from_int "(IZR %1)"
remove prop Zero
remove prop One
remove prop Add
remove prop Sub
remove prop Mul
remove prop Neg
end
theory real.Square
......@@ -187,6 +221,10 @@ theory real.Square
syntax function sqr "(Rsqr %1)"
syntax function sqrt "(sqrt %1)" (* and not Rsqrt *)
remove prop Sqrt_positive
remove prop Sqrt_square
remove prop Square_sqrt
end
......@@ -228,4 +266,14 @@ theory real.Trigonometry
syntax function tan "(Rtrigo.tan %1)"
(* syntax function atan "atan not defined in Coq ?" *)
remove prop Pythagorean_identity
remove prop Cos_le_one
remove prop Sin_le_one
remove prop Cos_0
remove prop Sin_0
remove prop Cos_pi
remove prop Sin_pi
remove prop Cos_pi2
remove prop Sin_pi2
end
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment