From d14635b0c74012e464aad9e77aeeffda0f1ef154 Mon Sep 17 00:00:00 2001 From: herbelin Date: Tue, 8 Jun 2010 13:56:14 +0000 Subject: Made option "Automatic Introduction" active by default before too many people use the undocumented "Lemma foo x : t" feature in a way incompatible with this activation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13090 85f007b7-540e-0410-9357-904b9bb8a0f7 --- theories/Setoids/Setoid.v | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'theories/Setoids') diff --git a/theories/Setoids/Setoid.v b/theories/Setoids/Setoid.v index cf641253a..e5c08335d 100644 --- a/theories/Setoids/Setoid.v +++ b/theories/Setoids/Setoid.v @@ -16,15 +16,15 @@ Definition Setoid_Theory := @Equivalence. Definition Build_Setoid_Theory := @Build_Equivalence. Definition Seq_refl A Aeq (s : Setoid_Theory A Aeq) : forall x:A, Aeq x x. - unfold Setoid_Theory. intros ; reflexivity. + unfold Setoid_Theory in s. intros ; reflexivity. Defined. Definition Seq_sym A Aeq (s : Setoid_Theory A Aeq) : forall x y:A, Aeq x y -> Aeq y x. - unfold Setoid_Theory. intros ; symmetry ; assumption. + unfold Setoid_Theory in s. intros ; symmetry ; assumption. Defined. Definition Seq_trans A Aeq (s : Setoid_Theory A Aeq) : forall x y z:A, Aeq x y -> Aeq y z -> Aeq x z. - unfold Setoid_Theory. intros ; transitivity y ; assumption. + unfold Setoid_Theory in s. intros ; transitivity y ; assumption. Defined. (** Some tactics for manipulating Setoid Theory not officially -- cgit v1.2.3