diff options
| author | bgregoir | 2006-12-11 18:46:35 +0000 |
|---|---|---|
| committer | bgregoir | 2006-12-11 18:46:35 +0000 |
| commit | c86d78c0f18fb28f74bb6b192c03ebe73117cf03 (patch) | |
| tree | 99294164215016607e4056e5730a2d6c91043dbf /contrib/setoid_ring/Ring.v | |
| parent | 70c88a5f6d7e1ef184d70512969a6221eec8d11e (diff) | |
Changement dans le kernel :
- essai de suppression des dependances debiles. (echec)
- Application des patch debian.
Pour ring et field :
- introduciton de la function de sign et de puissance.
- Correction de certains bug.
- supression de ring_replace ....
Pour exact_no_check :
- ajout de la tactic : vm_cast_no_check (t)
qui remplace "exact_no_check (t<: type of Goal)"
(cette version forcais l'evaluation du cast dans le
pretypage).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9427 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/setoid_ring/Ring.v')
| -rw-r--r-- | contrib/setoid_ring/Ring.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/contrib/setoid_ring/Ring.v b/contrib/setoid_ring/Ring.v index 167e026f61..1a4e1cc756 100644 --- a/contrib/setoid_ring/Ring.v +++ b/contrib/setoid_ring/Ring.v @@ -9,6 +9,7 @@ Require Import Bool. Require Export Ring_theory. Require Export Ring_base. +Require Export InitialRing. Require Export Ring_tac. Lemma BoolTheory : @@ -25,7 +26,7 @@ reflexivity. destruct x; reflexivity. Qed. -Unboxed Definition bool_eq (b1 b2:bool) := +Definition bool_eq (b1 b2:bool) := if b1 then b2 else negb b2. Lemma bool_eq_ok : forall b1 b2, bool_eq b1 b2 = true -> b1 = b2. |