Uniformisation convert_hyp

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

1 files changed, 16 insertions, 13 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 08ed47698..0d2a2f8f1 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -1681,13 +1681,14 @@ let rec decidability gl t =
 let destructure_hyps gl =
   let rec loop evbd = function
     | [] -> (tclTHEN nat_inject coq_omega)
-    | (i,t)::lit ->
+    | (i,body,t)::lit ->
 	begin try match destructurate t with
           | Kapp(("Zle"|"Zge"|"Zgt"|"Zlt"|"Zne"),[t1;t2]) -> loop evbd lit
           | Kapp("or",[t1;t2]) ->
               (tclTHENS ((tclTHEN ((tclTHEN (elim_id i) (clear [i]))) 
 			    (intros_using [i]))) 
-		 ([ loop evbd ((i,t1)::lit); loop evbd ((i,t2)::lit) ]))
+		 ([ loop evbd ((i,None,t1)::lit);
+                    loop evbd ((i,None,t2)::lit) ]))
           | Kapp("and",[t1;t2]) ->
               let i1 = id_of_string (string_of_id i ^ "_left") in
               let i2 = id_of_string (string_of_id i ^ "_right") in
@@ -1695,7 +1696,7 @@ let destructure_hyps gl =
 		 (tclTHEN 
 		    (tclTHEN (elim_id i) (clear [i]))
 		    (intros_using [i1;i2]))
-		 (loop (i1::i2::evbd) ((i1,t1)::(i2,t2)::lit)))
+		 (loop (i1::i2::evbd) ((i1,None,t1)::(i2,None,t2)::lit)))
           | Kimp(t1,t2) ->
               if isprop (pf_type_of gl t1) & closed0 t2 then begin
 		(tclTHEN 
@@ -1707,7 +1708,7 @@ let destructure_hyps gl =
 						    mkVar i|])]) 
 			 (clear [i])) 
 		      (intros_using [i])) 
-		   (loop evbd ((i,mk_or (mk_not t1) t2)::lit)))
+		   (loop evbd ((i,None,mk_or (mk_not t1) t2)::lit)))
               end else loop evbd lit
           | Kapp("not",[t]) -> 
               begin match destructurate t with 
@@ -1719,7 +1720,7 @@ let destructure_hyps gl =
 							t1; t2; mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i])) 
-                       (loop evbd ((i,mk_and (mk_not t1) (mk_not t2)):: lit)))
+                       (loop evbd ((i,None,mk_and (mk_not t1) (mk_not t2)):: lit)))
 		| Kapp("and",[t1;t2]) -> 
                     (tclTHEN 
 		       (tclTHEN 
@@ -1729,7 +1730,7 @@ let destructure_hyps gl =
 					   decidability gl t1;mkVar i|])])
 			     (clear [i]))
 			  (intros_using [i]))
-                       (loop evbd ((i,mk_or (mk_not t1) (mk_not t2))::lit)))
+                       (loop evbd ((i,None,mk_or (mk_not t1) (mk_not t2))::lit)))
 		| Kimp(t1,t2) ->
                     (tclTHEN 
 		       (tclTHEN 
@@ -1739,7 +1740,7 @@ let destructure_hyps gl =
 					   decidability gl t1;mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i]))
-                       (loop evbd ((i,mk_and t1 (mk_not t2)) :: lit)))
+                       (loop evbd ((i,None,mk_and t1 (mk_not t2)) :: lit)))
 		| Kapp("not",[t]) ->
                     (tclTHEN 
 		       (tclTHEN 
@@ -1749,7 +1750,7 @@ let destructure_hyps gl =
 					    decidability gl t; mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i])) 
-                       (loop evbd ((i,t)::lit)))
+                       (loop evbd ((i,None,t)::lit)))
 		| Kapp("Zle", [t1;t2]) ->
                     (tclTHEN 
 		       (tclTHEN 
@@ -1852,13 +1853,15 @@ let destructure_hyps gl =
 		      match destructurate (pf_nf gl typ) with
 			| Kapp("nat",_) -> 
                             (tclTHEN 
-			       (convert_hyp i 
-				  (mkApp (Lazy.force coq_neq, [| t1;t2|])))
+			       (convert_hyp
+                                  (i,body,
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|]))))
 			       (loop evbd lit))
 			| Kapp("Z",_) ->
                             (tclTHEN 
-			       (convert_hyp i 
-				  (mkApp (Lazy.force coq_Zne, [| t1;t2|])))
+			       (convert_hyp
+                                  (i,body,
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|]))))
 			       (loop evbd lit))
 			| _ -> loop evbd lit
                     end
@@ -1868,7 +1871,7 @@ let destructure_hyps gl =
 	with e when catchable_exception e -> loop evbd lit
 	end 
   in
-  loop (pf_ids_of_hyps gl) (pf_hyps_types gl) gl
+  loop (pf_ids_of_hyps gl) (pf_hyps gl) gl
 
 let destructure_goal gl =
   let concl = pf_concl gl in