diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 08:35:21 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-02-01 08:35:21 +0000 |
| commit | c300bc395fb987f7ded64c17bce5c966c0279442 (patch) | |
| tree | 443364b05d14feb412ba7a1a66ebc6ee1b6d8b2e /contrib | |
| parent | 1fda9cc1a2d8c2db92d88d3e2715d3ee86f90bf3 (diff) | |
- coqc : option -image
- coqmktop : manquaient des -I
- tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau
- correction d'un bug de Simpl avec Fix (découvert dans preuve FTA)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/omega/Zlogarithm.v | 4 | ||||
| -rw-r--r-- | contrib/ring/Ring.v | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/contrib/omega/Zlogarithm.v b/contrib/omega/Zlogarithm.v index 803981e33..5d343880e 100644 --- a/contrib/omega/Zlogarithm.v +++ b/contrib/omega/Zlogarithm.v @@ -140,10 +140,10 @@ Induction p; Simpl; Intros; [Elim p0; Auto with zarith | Elim p0; Auto with zarith | Trivial with zarith ]. Intros; Apply Zle_le_S. Generalize H0; Elim p1; Intros; Simpl; - [ Tauto | Tauto | Apply ZERO_le_POS ]. + [ Assumption | Assumption | Apply ZERO_le_POS ]. Intros; Apply Zle_le_S. Generalize H0; Elim p1; Intros; Simpl; - [ Tauto | Tauto | Apply ZERO_le_POS ]. + [ Assumption | Assumption | Apply ZERO_le_POS ]. Save. Theorem log_near_correct2: (p:positive) diff --git a/contrib/ring/Ring.v b/contrib/ring/Ring.v index 81b2077a4..b6f75a584 100644 --- a/contrib/ring/Ring.v +++ b/contrib/ring/Ring.v @@ -58,7 +58,7 @@ Destruct n; Reflexivity. Destruct n; Reflexivity. Destruct n; Reflexivity. Destruct n; Destruct m; Destruct p; Reflexivity. -Destruct x; Destruct y; Reflexivity Orelse Tauto. +Destruct x; Destruct y; Reflexivity Orelse Simpl; Tauto. Defined. Add Ring bool xorb andb true false [b:bool]b eqb BoolTheory [ true false ]. |