Modification de l'emplacement des fichiers pour les setoides.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1982 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 31 insertions, 29 deletions

diff --git a/theories/Setoid/Setoid_replace.v b/theories/Init/Setoid.v
index ba4e829f18..c09888ac3d 100644
--- a/theories/Setoid/Setoid_replace.v
+++ b/theories/Init/Setoid.v
@@ -8,29 +8,9 @@
 
 (* $Id$: *)
 
-Declare ML Module "setoid_replace".
-
-Grammar tactic simple_tactic : ast :=
-  setoid_replace [ "Setoid_replace" constrarg($c1) "with" constrarg($c2) ] -> [(Setoid_replace $c1 $c2)]
-.
-
-Grammar tactic simple_tactic : ast :=
-  setoid_rewriteLR [ "Setoid_rewrite" "->" constrarg($c) ] -> [(Setoid_rewriteLR $c)]
-| setoid_rewriteRL [ "Setoid_rewrite" "<-" constrarg($c) ] -> [(Setoid_rewriteRL $c)]
-| setoid_rewrite [ "Setoid_rewrite" constrarg($c) ] -> [(Setoid_rewriteLR $c)]
-.
-
-Syntax tactic level 0 :
-  setoid_replace [<<(Setoid_replace  $c1 $c2)>>] -> [[<hov 0>"Setoid_replace " $c1 [1 1] "with " $c2]]
- | setoid_rewritelr [<<(Setoid_rewriteLR  $c)>>] -> ["Setoid_rewrite " $c]
- | setoid_rewriterl [<<(Setoid_rewriteRL  $c)>>] -> ["Setoid_rewrite <- " $c]
-.
-
-Grammar vernac vernac : ast :=
-  add_setoid [ "Add" "Setoid" constrarg($a) constrarg($aeq) constrarg($t) "." ] 
-    -> [(AddSetoid $a $aeq $t)]
-| new_morphism [ "Add" "Morphism" constrarg($m) ":" identarg($s) "." ] -> [(NamedNewMorphism $s $m)]
-.
+Require Logic.
+Require Export Setoid_replace.
+Require Inv.
 
 Section Setoid.
 
@@ -45,8 +25,8 @@ Record Setoid_Theory : Prop :=
 
 End Setoid.
 
-Definition Prop_S : (Setoid_Theory Prop ([x,y:Prop] x<->y)).
-Split; Tauto.
+Definition Prop_S : (Setoid_Theory Prop iff).
+Split; [Exact iff_refl | Exact iff_sym | Exact iff_trans].
 Save.
 
 Add Setoid Prop iff Prop_S.
@@ -56,20 +36,42 @@ Hint prop_set : setoid := Resolve (Seq_sym Prop iff Prop_S).
 Hint prop_set : setoid := Resolve (Seq_trans Prop iff Prop_S).
 
 Add Morphism or : or_ext.
-Tauto.
+Intros.
+Inversion H1.
+Left.
+Inversion H.
+Apply (H3 H2).
+
+Right.
+Inversion H0.
+Apply (H3 H2).
 Save.
 
 Add Morphism and : and_ext.
-Tauto.
+Intros.
+Inversion H1.
+Split.
+Inversion H.
+Apply (H4 H2).
+
+Inversion H0.
+Apply (H4 H3).
 Save.
 
 Add Morphism not : not_ext.
-Tauto.
+Red ; Intros.
+Apply H0.
+Inversion H.
+Apply (H3 H1).
 Save.
 
 Definition fleche [A,B:Prop] := A -> B.
 
 Add Morphism fleche : fleche_ext.
-Tauto.
+Unfold fleche.
+Intros.
+Inversion H0.
+Inversion H.
+Apply (H3 (H1 (H6 H2))).
 Save.