Omega échouait à effacer les hypothèses à contenu arithmétique lorsque ces hypothèses étaient dépendantes dans d'autres hypothèses

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

2 files changed, 29 insertions, 12 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index f867d203bc..f26d0dc2ab 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1335,6 +1335,10 @@ let destructure_omega gl tac_def (id,c) =
       | _ -> tac_def
     with e when catchable_exception e -> tac_def
 
+let reintroduce id =
+  (* [id] cannot be cleared if dependent: protect it by a try *)
+  tclTHEN (tclTRY (clear [id])) (intro_using id)
+      
 let coq_omega gl =
   clear_tables ();
   let tactic_normalisation, system = 
@@ -1462,8 +1466,7 @@ let nat_inject gl =
 		    [mkApp (Lazy.force coq_inj_le, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
-		  (clear [i]);
-                  (intros_using [i]);
+		  (reintroduce i);
 		  (loop lit)
                 ]
             | Kapp("lt",[t1;t2]) ->
@@ -1472,8 +1475,7 @@ let nat_inject gl =
 		    [mkApp (Lazy.force coq_inj_lt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
-		  (clear [i]);
-		  (intros_using [i]);
+		  (reintroduce i);
 		  (loop lit)
                 ]
             | Kapp("ge",[t1;t2]) ->
@@ -1482,8 +1484,7 @@ let nat_inject gl =
 		    [mkApp (Lazy.force coq_inj_ge, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
-		  (clear [i]);
-		  (intros_using [i]);
+		  (reintroduce i);
 		  (loop lit)
                 ]
             | Kapp("gt",[t1;t2]) ->
@@ -1492,8 +1493,7 @@ let nat_inject gl =
                     [mkApp (Lazy.force coq_inj_gt, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
-		  (clear [i]);
-		  (intros_using [i]);
+		  (reintroduce i);
 		  (loop lit)
                 ]
             | Kapp("neq",[t1;t2]) ->
@@ -1502,8 +1502,7 @@ let nat_inject gl =
 		    [mkApp (Lazy.force coq_inj_neq, [| t1;t2;mkVar i |]) ]);
 		  (explore [P_APP 1; P_TYPE] t1);
 		  (explore [P_APP 2; P_TYPE] t2);
-		  (clear [i]);
-		  (intros_using [i]);
+		  (reintroduce i);
 		  (loop lit)
 ]
             | Kapp("eq",[typ;t1;t2]) ->
@@ -1513,8 +1512,7 @@ let nat_inject gl =
 		      [mkApp (Lazy.force coq_inj_eq, [| t1;t2;mkVar i |]) ]);
 		    (explore [P_APP 2; P_TYPE] t1);
 		    (explore [P_APP 3; P_TYPE] t2);
-		    (clear [i]);
-		    (intros_using [i]);
+		    (reintroduce i);
 		    (loop lit)
                   ]
 		else loop lit
diff --git a/test-suite/success/Omega.v b/test-suite/success/Omega.v
index 19bb5f809c..680012462c 100644
--- a/test-suite/success/Omega.v
+++ b/test-suite/success/Omega.v
@@ -52,3 +52,22 @@ Lemma lem5 : `H > 0`.
 Omega.
 Qed.
 End B.
+
+(* From Nicolas Oury (bug #180): handling -> on Set (fixed Oct 2002) *)
+Lemma lem7: (A: Set) (i:Z) `i<= 0` -> (`i<= 0` -> A) -> `i<=0`.
+Intros.
+Omega.
+Qed.
+
+(* Adapted from an example in Nijmegen/FTA/ftc/RefSeparating (Oct 2002) *)
+Require Omega.
+Section C.
+Parameter g:(m:nat)~m=O->Prop.
+Parameter f:(m:nat)(H:~m=O)(g m H).
+Variable n:nat.
+Variable ap_n:~n=O.
+Local delta:=(f n ap_n).
+Lemma lem6 : n=n.
+Omega.
+Qed.
+End C.