From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Sat, 6 Jan 2007 16:14:06 +0000 (+0000)
Subject: ;auto fixed
X-Git-Tag: 0.4.95@7852~677
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=2f857bf7f4d1bb73d08d270af9d7ad36a365a3c4;p=helm.git

;auto fixed
---

diff --git a/matita/contribs/RELATIONAL/NLE/fwd.ma b/matita/contribs/RELATIONAL/NLE/fwd.ma
index 5ddeb41af..afefbfd4d 100644
--- a/matita/contribs/RELATIONAL/NLE/fwd.ma
+++ b/matita/contribs/RELATIONAL/NLE/fwd.ma
@@ -25,7 +25,7 @@ theorem nle_gen_succ_1: \forall x,y. x < y \to
  intros. decompose.
  lapply linear nplus_gen_succ_2 to H1 as H.
  decompose. subst.
- apply ex_intro; auto. (**)
+ apply ex_intro;[| auto] (**)
 qed.
 
 
diff --git a/matita/contribs/RELATIONAL/NLE/props.ma b/matita/contribs/RELATIONAL/NLE/props.ma
index b571dfc6b..549eae418 100644
--- a/matita/contribs/RELATIONAL/NLE/props.ma
+++ b/matita/contribs/RELATIONAL/NLE/props.ma
@@ -24,7 +24,7 @@ qed.
 theorem nle_succ: \forall p,q. p <= q \to succ p <= succ q.
  unfold NLE.
  intros. decompose.
- apply ex_intro; auto. (**)
+ apply ex_intro; [|auto] (**)
 qed.
 
 theorem nle_refl: \forall x. x <= x.