Renommage AppL en App

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

1 files changed, 88 insertions, 88 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 963f418218..06c404aefb 100644
--- a/contrib/omega/coq_omega.ml
+++ b/contrib/omega/coq_omega.ml
@@ -392,28 +392,28 @@ let sp_Zlt = path_of_string "#zarith_aux#Zlt.cci"
 let sp_not = path_of_string "#Logic#not.cci"
 
 let mk_var v = mkVar (id_of_string v)
-let mk_plus t1 t2 = mkAppL (Lazy.force coq_Zplus, [| t1; t2 |])
-let mk_times t1 t2 = mkAppL (Lazy.force coq_Zmult, [| t1; t2 |])
-let mk_minus t1 t2 = mkAppL (Lazy.force coq_Zminus, [| t1;t2 |])
-let mk_eq t1 t2 = mkAppL (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |])
-let mk_le t1 t2 = mkAppL (Lazy.force coq_Zle, [| t1; t2 |])
-let mk_gt t1 t2 = mkAppL (Lazy.force coq_Zgt, [| t1; t2 |])
-let mk_inv t = mkAppL (Lazy.force coq_Zopp, [| t |])
-let mk_and t1 t2 =  mkAppL (Lazy.force coq_and, [| t1; t2 |])
-let mk_or t1 t2 =  mkAppL (Lazy.force coq_or, [| t1; t2 |])
-let mk_not t = mkAppL (Lazy.force coq_not, [| t |])
-let mk_eq_rel t1 t2 = mkAppL (Lazy.force coq_eq,
+let mk_plus t1 t2 = mkApp (Lazy.force coq_Zplus, [| t1; t2 |])
+let mk_times t1 t2 = mkApp (Lazy.force coq_Zmult, [| t1; t2 |])
+let mk_minus t1 t2 = mkApp (Lazy.force coq_Zminus, [| t1;t2 |])
+let mk_eq t1 t2 = mkApp (Lazy.force coq_eq, [| Lazy.force coq_Z; t1; t2 |])
+let mk_le t1 t2 = mkApp (Lazy.force coq_Zle, [| t1; t2 |])
+let mk_gt t1 t2 = mkApp (Lazy.force coq_Zgt, [| t1; t2 |])
+let mk_inv t = mkApp (Lazy.force coq_Zopp, [| t |])
+let mk_and t1 t2 =  mkApp (Lazy.force coq_and, [| t1; t2 |])
+let mk_or t1 t2 =  mkApp (Lazy.force coq_or, [| t1; t2 |])
+let mk_not t = mkApp (Lazy.force coq_not, [| t |])
+let mk_eq_rel t1 t2 = mkApp (Lazy.force coq_eq,
 			      [| Lazy.force coq_relation; t1; t2 |])
-let mk_inj t = mkAppL (Lazy.force coq_inject_nat, [| t |])
+let mk_inj t = mkApp (Lazy.force coq_inject_nat, [| t |])
 
 let mk_integer n =
   let rec loop n = 
     if n=1 then Lazy.force coq_xH else 
-      mkAppL ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI),
+      mkApp ((if n mod 2 = 0 then Lazy.force coq_xO else Lazy.force coq_xI),
 		[| loop (n/2) |])
   in
   if n = 0 then Lazy.force coq_ZERO 
-  else mkAppL ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG),
+  else mkApp ((if n > 0 then Lazy.force coq_POS else Lazy.force coq_NEG),
 		 [| loop (abs n) |])
     
 type constr_path =
@@ -431,20 +431,20 @@ let context operation path (t : constr) =
     match (p0,kind_of_term t) with 
       | (p, IsCast (c,t)) -> mkCast (loop i p c,t)
       | ([], _) -> operation i t
-      | ((P_APP n :: p),  IsAppL (f,v)) ->
+      | ((P_APP n :: p),  IsApp (f,v)) ->
 (*	  let f,l = get_applist t in   NECESSAIRE ??
 	  let v' = Array.of_list (f::l) in  *)
 	  let v' = Array.copy v in
-	  v'.(n-1) <- loop i p v'.(n-1); mkAppL (f, v')
+	  v'.(n-1) <- loop i p v'.(n-1); mkApp (f, v')
       | ((P_BRANCH n :: p), IsMutCase (ci,q,c,v)) ->
-	  (* avant, y avait mkAppL... anyway, BRANCH seems nowhere used *)
+	  (* avant, y avait mkApp... anyway, BRANCH seems nowhere used *)
 	  let v' = Array.copy v in
 	  v'.(n) <- loop i p v'.(n); (mkMutCase (ci,q,c,v'))
-      | ((P_ARITY :: p),  IsAppL (f,l)) ->
+      | ((P_ARITY :: p),  IsApp (f,l)) ->
 	  appvect (loop i p f,l)
-      | ((P_ARG :: p),  IsAppL (f,v)) ->
+      | ((P_ARG :: p),  IsApp (f,v)) ->
 	  let v' = Array.copy v in
-	  v'.(0) <- loop i p v'.(0); mkAppL (f,v')
+	  v'.(0) <- loop i p v'.(0); mkApp (f,v')
       | (p, IsFix ((_,n as ln),(tys,lna,v))) ->
 	  let l = Array.length v in
 	  let v' = Array.copy v in
@@ -471,10 +471,10 @@ let occurence path (t : constr) =
   let rec loop p0 t = match (p0,kind_of_term t) with
     | (p, IsCast (c,t)) -> loop p c
     | ([], _) -> t
-    | ((P_APP n :: p),  IsAppL (f,v)) -> loop p v.(n-1)
+    | ((P_APP n :: p),  IsApp (f,v)) -> loop p v.(n-1)
     | ((P_BRANCH n :: p), IsMutCase (_,_,_,v)) -> loop p v.(n)
-    | ((P_ARITY :: p),  IsAppL (f,_)) -> loop p f
-    | ((P_ARG :: p),  IsAppL (f,v)) -> loop p v.(0)
+    | ((P_ARITY :: p),  IsApp (f,_)) -> loop p f
+    | ((P_ARG :: p),  IsApp (f,v)) -> loop p v.(0)
     | (p, IsFix((_,n) ,(_,_,v))) -> loop p v.(n)
     | ((P_BODY :: p), IsProd (n,t,c)) -> loop p c
     | ((P_BODY :: p), IsLambda (n,t,c)) -> loop p c
@@ -530,9 +530,9 @@ let rec weight = function
 let rec val_of = function
   | Oatom c -> (mkVar (id_of_string c))
   | Oz c -> mk_integer c
-  | Oinv c -> mkAppL (Lazy.force coq_Zopp, [| val_of c |])
-  | Otimes (t1,t2) -> mkAppL (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
-  | Oplus(t1,t2) -> mkAppL (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
+  | Oinv c -> mkApp (Lazy.force coq_Zopp, [| val_of c |])
+  | Otimes (t1,t2) -> mkApp (Lazy.force coq_Zmult, [| val_of t1; val_of t2 |])
+  | Oplus(t1,t2) -> mkApp (Lazy.force coq_Zplus, [| val_of t1; val_of t2 |])
   | Oufo c -> c
 
 let compile name kind = 
@@ -566,7 +566,7 @@ let clever_rewrite_base_poly typ p result theorem gl =
           mkLambda
 	    (Name (id_of_string "H"),
 	     applist (mkRel 1,[result]),
-	     mkAppL (Lazy.force coq_eq_ind_r, 
+	     mkApp (Lazy.force coq_eq_ind_r, 
 		       [| typ; result; mkRel 2; mkRel 1; occ; theorem |]))),
        [abstracted]) 
   in
@@ -777,7 +777,7 @@ let rec scalar p n = function
   | Otimes(t1,t2) -> error "Omega: Can't solve a goal with non-linear products"
   | (Oatom _ as t) -> [], Otimes(t,Oz n)
   | Oz i -> [focused_simpl p],Oz(n*i)
-  | Oufo c -> [], Oufo (mkAppL (Lazy.force coq_Zmult, [| mk_integer n |]))
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zmult, [| mk_integer n |]))
       
 let rec scalar_norm p_init = 
   let rec loop p = function
@@ -831,7 +831,7 @@ let rec negate p = function
       let r = Otimes(t,Oz(-1)) in
       [clever_rewrite p [[P_APP 1]] (Lazy.force coq_fast_Zopp_one)], r
   | Oz i -> [focused_simpl p],Oz(-i)
-  | Oufo c -> [], Oufo (mkAppL (Lazy.force coq_Zopp, [| c |]))
+  | Oufo c -> [], Oufo (mkApp (Lazy.force coq_Zopp, [| c |]))
       
 let rec transform p t = 
   let default () =
@@ -853,11 +853,11 @@ let rec transform p t =
     | Kapp("Zminus",[t1;t2]) ->
 	let tac,t = 
 	  transform p
-	    (mkAppL (Lazy.force coq_Zplus,
-		     [| t1; (mkAppL (Lazy.force coq_Zopp, [| t2 |])) |])) in
+	    (mkApp (Lazy.force coq_Zplus,
+		     [| t1; (mkApp (Lazy.force coq_Zopp, [| t2 |])) |])) in
 	unfold sp_Zminus :: tac,t
     | Kapp("Zs",[t1]) ->
-	let tac,t = transform p (mkAppL (Lazy.force coq_Zplus,
+	let tac,t = transform p (mkApp (Lazy.force coq_Zplus,
 					 [| t1; mk_integer 1 |])) in
 	unfold sp_Zs :: tac,t
    | Kapp("Zmult",[t1;t2]) ->
@@ -1001,7 +1001,7 @@ let replay_history tactic_normalisation =
 	       (tclTHEN 
 		  (tclTHEN 
 		     (generalize_tac 
-			[mkAppL (Lazy.force coq_OMEGA17, [| 
+			[mkApp (Lazy.force coq_OMEGA17, [| 
 				   val_of eq1;
 				   val_of eq2;
 				   mk_integer k; 
@@ -1017,7 +1017,7 @@ let replay_history tactic_normalisation =
 	  let tac = shuffle_cancel p_initial e1.body in
 	  let solve_le =
             let superieur = Lazy.force coq_SUPERIEUR in
-            let not_sup_sup = mkAppL (Lazy.force coq_eq, [| 
+            let not_sup_sup = mkApp (Lazy.force coq_eq, [| 
 					Lazy.force coq_relation; 
 					Lazy.force coq_SUPERIEUR;
 					Lazy.force coq_SUPERIEUR |])
@@ -1033,7 +1033,7 @@ let replay_history tactic_normalisation =
 	      [ assumption ; reflexivity ] 
 	  in
 	  let theorem =
-            mkAppL (Lazy.force coq_OMEGA2, [| 
+            mkApp (Lazy.force coq_OMEGA2, [| 
 		      val_of eq1; val_of eq2; 
 		      mkVar (hyp_of_tag e1.id);
 		      mkVar (hyp_of_tag e2.id) |])
@@ -1057,7 +1057,7 @@ let replay_history tactic_normalisation =
 			 (tclTHEN 
 			    (intros_using [aux])
 			    (generalize_tac 
-			       [mkAppL (Lazy.force coq_OMEGA1,
+			       [mkApp (Lazy.force coq_OMEGA1,
 					[| eq1; rhs; mkVar aux; mkVar id |])]))
 			 (clear [aux;id])) 
 		      (intros_using [id]))
@@ -1070,7 +1070,7 @@ let replay_history tactic_normalisation =
 			      (tclTHEN 
 				 (intros_using [aux1; aux2])
 				 (generalize_tac 
-				    [mkAppL (Lazy.force coq_Zmult_le_approx, [|
+				    [mkApp (Lazy.force coq_Zmult_le_approx, [|
 				       kk;eq2;dd;mkVar aux1;mkVar aux2; 
 				       mkVar id |])]))
 			      (clear [aux1;aux2;id])) 
@@ -1110,7 +1110,7 @@ let replay_history tactic_normalisation =
 				  (tclTHEN 
 				     (intros_using [aux2;aux1])
 				     (generalize_tac 
-					[mkAppL (Lazy.force coq_OMEGA4, [|
+					[mkApp (Lazy.force coq_OMEGA4, [|
 						   dd;kk;eq2;mkVar aux1; 
 						   mkVar aux2 |])]))
 				  (clear [aux1;aux2])) 
@@ -1145,7 +1145,7 @@ let replay_history tactic_normalisation =
 		       (tclTHEN 
 			  (intros_using [aux1])
 			  (generalize_tac 
-			     [mkAppL (Lazy.force coq_OMEGA18, [| 
+			     [mkApp (Lazy.force coq_OMEGA18, [| 
 				eq1;eq2;kk;mkVar aux1; mkVar id |])]))
 		       (clear [aux1;id]))
 		    (intros_using [id])) 
@@ -1163,7 +1163,7 @@ let replay_history tactic_normalisation =
 			  (tclTHEN 
 			     (intros_using [aux2;aux1])
 			     (generalize_tac 
-				[mkAppL (Lazy.force coq_OMEGA3, [| 
+				[mkApp (Lazy.force coq_OMEGA3, [| 
 					   eq1; eq2; kk; mkVar aux2; 
 					   mkVar aux1;mkVar id|])]))
 			  (clear [aux1;aux2;id]))
@@ -1192,7 +1192,7 @@ let replay_history tactic_normalisation =
 		  (tclTHEN
 		     (tclTHEN 
 			(intros_using [aux])
-			(generalize_tac [mkAppL (Lazy.force coq_OMEGA8, [| 
+			(generalize_tac [mkApp (Lazy.force coq_OMEGA8, [| 
 					   eq1;eq2;mkVar id1;mkVar id2; 
 					   mkVar aux|])]))
 		     (clear [id1;id2;aux]))
@@ -1209,7 +1209,7 @@ let replay_history tactic_normalisation =
 	  let v = unintern_id sigma in
 	  let vid = id_of_string v in
 	  let theorem =
-            mkAppL (Lazy.force coq_ex, [| 
+            mkApp (Lazy.force coq_ex, [| 
 		      Lazy.force coq_Z;
 		      mkLambda
 			(Name(id_of_string v),
@@ -1239,7 +1239,7 @@ let replay_history tactic_normalisation =
 				 (clear [aux]))
 			      (intros_using [vid; aux]))
 			   (generalize_tac
-			      [mkAppL (Lazy.force coq_OMEGA9, [| 
+			      [mkApp (Lazy.force coq_OMEGA9, [| 
 					 mkVar vid;eq2;eq1;mm;
 					 mkVar id2;mkVar aux |])]))
 			(mk_then tac)) 
@@ -1282,7 +1282,7 @@ let replay_history tactic_normalisation =
             tclTHEN 
 	      (tclTHEN 
 		 (tclTHEN 
-		    (generalize_tac [mkAppL (tac_thm, [| eq1; eq2; 
+		    (generalize_tac [mkApp (tac_thm, [| eq1; eq2; 
 					       kk; mkVar id1; mkVar id2 |])])
 		    (mk_then tac)) 
 		 (intros_using [id])) 
@@ -1302,7 +1302,7 @@ let replay_history tactic_normalisation =
 			     (tclTHEN 
 				(intros_using [aux2;aux1]) 
 				(generalize_tac
-				   [mkAppL (Lazy.force coq_OMEGA7, [| 
+				   [mkApp (Lazy.force coq_OMEGA7, [| 
 					      eq1;eq2;kk1;kk2; 
 					      mkVar aux1;mkVar aux2;
 					      mkVar id1;mkVar id2 |])]))
@@ -1349,7 +1349,7 @@ let normalize_equation id flag theorem pos t t1 t2 (tactic,defs) =
   let (tac,t') = normalize p_initial t in
   let shift_left = 
     tclTHEN 
-      (generalize_tac [mkAppL (theorem, [| t1; t2; mkVar id |]) ])
+      (generalize_tac [mkApp (theorem, [| t1; t2; mkVar id |]) ])
       (clear [id]) 
   in
   if tac <> [] then
@@ -1478,14 +1478,14 @@ let nat_inject gl =
 		       (clever_rewrite_gen p 
 			  (mk_minus (mk_inj t1) (mk_inj t2))
                           ((Lazy.force coq_inj_minus1),[t1;t2;mkVar id]))
-		       (loop [id,mkAppL (Lazy.force coq_le, [| t2;t1 |])]))
+		       (loop [id,mkApp (Lazy.force coq_le, [| t2;t1 |])]))
 		    (explore (P_APP 1 :: p) t1)) 
 		 (explore (P_APP 2 :: p) t2));
 	      
 	      (tclTHEN 
 		 (clever_rewrite_gen p (mk_integer 0)
                     ((Lazy.force coq_inj_minus2),[t1;t2;mkVar id]))
-		 (loop [id,mkAppL (Lazy.force coq_gt, [| t2;t1 |])]))
+		 (loop [id,mkApp (Lazy.force coq_gt, [| t2;t1 |])]))
 	    ]
       | Kapp("S",[t']) ->
           let rec is_number t =
@@ -1500,7 +1500,7 @@ let nat_inject gl =
 		Kapp("S",[t]) ->
                   (tclTHEN 
                      (clever_rewrite_gen p 
-			(mkAppL (Lazy.force coq_Zs, [| mk_inj t |]))
+			(mkApp (Lazy.force coq_Zs, [| mk_inj t |]))
 			((Lazy.force coq_inj_S),[t])) 
 		     (loop (P_APP 1 :: p) t))
               | _ -> explore p t 
@@ -1509,8 +1509,8 @@ let nat_inject gl =
           if is_number t' then focused_simpl p else loop p t
       | Kapp("pred",[t]) ->
           let t_minus_one = 
-	    mkAppL (Lazy.force coq_minus, [| t; 
-		      mkAppL (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
+	    mkApp (Lazy.force coq_minus, [| t; 
+		      mkApp (Lazy.force coq_S, [| Lazy.force coq_O |]) |]) in
           tclTHEN
             (clever_rewrite_gen_nat (P_APP 1 :: p) t_minus_one 
                ((Lazy.force coq_pred_of_minus),[t]))
@@ -1530,7 +1530,7 @@ let nat_inject gl =
 			 (tclTHEN 
 			    (tclTHEN 
 			       (generalize_tac 
-				  [mkAppL (Lazy.force coq_inj_le,
+				  [mkApp (Lazy.force coq_inj_le,
 					     [| t1;t2;mkVar i |]) ])
 			       (explore [P_APP 1; P_TYPE] t1))
 			    (explore [P_APP 2; P_TYPE] t2))
@@ -1544,7 +1544,7 @@ let nat_inject gl =
 			 (tclTHEN 
 			    (tclTHEN 
 			       (generalize_tac 
-				  [mkAppL (Lazy.force coq_inj_lt, [|  
+				  [mkApp (Lazy.force coq_inj_lt, [|  
 					     t1;t2;mkVar i |]) ])
 			       (explore [P_APP 1; P_TYPE] t1))
 			    (explore [P_APP 2; P_TYPE] t2))
@@ -1558,7 +1558,7 @@ let nat_inject gl =
 			 (tclTHEN 
 			    (tclTHEN 
 			       (generalize_tac 
-				  [mkAppL (Lazy.force coq_inj_ge,
+				  [mkApp (Lazy.force coq_inj_ge,
 					     [| t1;t2;mkVar i |]) ])
 			       (explore [P_APP 1; P_TYPE] t1))
 			    (explore [P_APP 2; P_TYPE] t2))
@@ -1572,7 +1572,7 @@ let nat_inject gl =
 			 (tclTHEN 
 			    (tclTHEN 
 			       (generalize_tac 
-				  [mkAppL (Lazy.force coq_inj_gt, [|  
+				  [mkApp (Lazy.force coq_inj_gt, [|  
 					     t1;t2;mkVar i |]) ])
 			       (explore [P_APP 1; P_TYPE] t1))
 			    (explore [P_APP 2; P_TYPE] t2))
@@ -1586,7 +1586,7 @@ let nat_inject gl =
 			 (tclTHEN 
 			    (tclTHEN 
 			       (generalize_tac 
-				  [mkAppL (Lazy.force coq_inj_neq, [| 
+				  [mkApp (Lazy.force coq_inj_neq, [| 
 					     t1;t2;mkVar i |]) ])
 			       (explore [P_APP 1; P_TYPE] t1))
 			    (explore [P_APP 2; P_TYPE] t2))
@@ -1601,7 +1601,7 @@ let nat_inject gl =
 			   (tclTHEN 
 			      (tclTHEN
 				 (generalize_tac 
-				    [mkAppL (Lazy.force coq_inj_eq, [| 
+				    [mkApp (Lazy.force coq_inj_eq, [| 
 					       t1;t2;mkVar i |]) ])
 				 (explore [P_APP 2; P_TYPE] t1))
 			      (explore [P_APP 3; P_TYPE] t2))
@@ -1617,33 +1617,33 @@ let nat_inject gl =
 let rec decidability gl t =
   match destructurate t with
     | Kapp("or",[t1;t2]) -> 
-	mkAppL (Lazy.force coq_dec_or, [| t1; t2;
+	mkApp (Lazy.force coq_dec_or, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
     | Kapp("and",[t1;t2]) -> 
-	mkAppL (Lazy.force coq_dec_and, [| t1; t2;
+	mkApp (Lazy.force coq_dec_and, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
     | Kimp(t1,t2) -> 
-	mkAppL (Lazy.force coq_dec_imp, [| t1; t2;
+	mkApp (Lazy.force coq_dec_imp, [| t1; t2;
 		  decidability gl t1; decidability gl t2 |])
-    | Kapp("not",[t1]) -> mkAppL (Lazy.force coq_dec_not, [| t1; 
+    | Kapp("not",[t1]) -> mkApp (Lazy.force coq_dec_not, [| t1; 
 				    decidability gl t1 |])
     | Kapp("eq",[typ;t1;t2]) -> 
 	begin match destructurate (pf_nf gl typ) with
-          | Kapp("Z",[]) ->  mkAppL (Lazy.force coq_dec_eq, [| t1;t2 |])
-          | Kapp("nat",[]) ->  mkAppL (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
+          | Kapp("Z",[]) ->  mkApp (Lazy.force coq_dec_eq, [| t1;t2 |])
+          | Kapp("nat",[]) ->  mkApp (Lazy.force coq_dec_eq_nat, [| t1;t2 |])
           | _ -> errorlabstrm "decidability" 
 		[< 'sTR "Omega: Can't solve a goal with equality on "; 
 		   Printer.prterm typ >]
 	end
-    | Kapp("Zne",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zne, [| t1;t2 |])
-    | Kapp("Zle",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zle, [| t1;t2 |])
-    | Kapp("Zlt",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zlt, [| t1;t2 |])
-    | Kapp("Zge",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zge, [| t1;t2 |])
-    | Kapp("Zgt",[t1;t2]) -> mkAppL (Lazy.force coq_dec_Zgt, [| t1;t2 |])
-    | Kapp("le", [t1;t2]) -> mkAppL (Lazy.force coq_dec_le, [| t1;t2 |])
-    | Kapp("lt", [t1;t2]) -> mkAppL (Lazy.force coq_dec_lt, [| t1;t2 |])
-    | Kapp("ge", [t1;t2]) -> mkAppL (Lazy.force coq_dec_ge, [| t1;t2 |])
-    | Kapp("gt", [t1;t2]) -> mkAppL (Lazy.force coq_dec_gt, [| t1;t2 |])
+    | Kapp("Zne",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zne, [| t1;t2 |])
+    | Kapp("Zle",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zle, [| t1;t2 |])
+    | Kapp("Zlt",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zlt, [| t1;t2 |])
+    | Kapp("Zge",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zge, [| t1;t2 |])
+    | Kapp("Zgt",[t1;t2]) -> mkApp (Lazy.force coq_dec_Zgt, [| t1;t2 |])
+    | Kapp("le", [t1;t2]) -> mkApp (Lazy.force coq_dec_le, [| t1;t2 |])
+    | Kapp("lt", [t1;t2]) -> mkApp (Lazy.force coq_dec_lt, [| t1;t2 |])
+    | Kapp("ge", [t1;t2]) -> mkApp (Lazy.force coq_dec_ge, [| t1;t2 |])
+    | Kapp("gt", [t1;t2]) -> mkApp (Lazy.force coq_dec_gt, [| t1;t2 |])
     | Kapp("False",[]) -> Lazy.force coq_dec_False
     | Kapp("True",[]) -> Lazy.force coq_dec_True
     | Kapp(t,_::_) -> error ("Omega: Unrecognized predicate or connective: "
@@ -1675,7 +1675,7 @@ let destructure_hyps gl =
 		(tclTHEN 
 		   (tclTHEN 
 		      (tclTHEN
-			 (generalize_tac [mkAppL (Lazy.force coq_imp_simp, [| 
+			 (generalize_tac [mkApp (Lazy.force coq_imp_simp, [| 
 						    t1; t2; 
 						    decidability gl t1;
 						    mkVar i|])]) 
@@ -1689,7 +1689,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN 
-			     (generalize_tac [mkAppL (Lazy.force coq_not_or,[| 
+			     (generalize_tac [mkApp (Lazy.force coq_not_or,[| 
 							t1; t2; mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1699,7 +1699,7 @@ let destructure_hyps gl =
 		       (tclTHEN 
 			  (tclTHEN
 			     (generalize_tac
-				[mkAppL (Lazy.force coq_not_and, [| t1; t2;
+				[mkApp (Lazy.force coq_not_and, [| t1; t2;
 					   decidability gl t1;mkVar i|])])
 			     (clear [i]))
 			  (intros_using [i]))
@@ -1709,7 +1709,7 @@ let destructure_hyps gl =
 		       (tclTHEN 
 			  (tclTHEN
 			     (generalize_tac 
-				[mkAppL (Lazy.force coq_not_imp, [| t1; t2; 
+				[mkApp (Lazy.force coq_not_imp, [| t1; t2; 
 					   decidability gl t1;mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i]))
@@ -1719,7 +1719,7 @@ let destructure_hyps gl =
 		       (tclTHEN 
 			  (tclTHEN
 			     (generalize_tac
-				[mkAppL (Lazy.force coq_not_not, [| t;
+				[mkApp (Lazy.force coq_not_not, [| t;
 					    decidability gl t; mkVar i |])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1728,7 +1728,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_Zle,
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zle,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1737,7 +1737,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_Zge,
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zge,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1746,7 +1746,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_Zlt,
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zlt,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1755,7 +1755,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_Zgt,
+			     (generalize_tac [mkApp (Lazy.force coq_not_Zgt,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1764,7 +1764,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_le,
+			     (generalize_tac [mkApp (Lazy.force coq_not_le,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1773,7 +1773,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_ge,
+			     (generalize_tac [mkApp (Lazy.force coq_not_ge,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1782,7 +1782,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_lt,
+			     (generalize_tac [mkApp (Lazy.force coq_not_lt,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1791,7 +1791,7 @@ let destructure_hyps gl =
                     (tclTHEN 
 		       (tclTHEN 
 			  (tclTHEN
-			     (generalize_tac [mkAppL (Lazy.force coq_not_gt,
+			     (generalize_tac [mkApp (Lazy.force coq_not_gt,
 							[| t1;t2;mkVar i|])])
 			     (clear [i])) 
 			  (intros_using [i])) 
@@ -1827,12 +1827,12 @@ let destructure_hyps gl =
 			| Kapp("nat",_) -> 
                             (tclTHEN 
 			       (convert_hyp i 
-				  (mkAppL (Lazy.force coq_neq, [| t1;t2|])))
+				  (mkApp (Lazy.force coq_neq, [| t1;t2|])))
 			       (loop evbd lit))
 			| Kapp("Z",_) ->
                             (tclTHEN 
 			       (convert_hyp i 
-				  (mkAppL (Lazy.force coq_Zne, [| t1;t2|])))
+				  (mkApp (Lazy.force coq_Zne, [| t1;t2|])))
 			       (loop evbd lit))
 			| _ -> loop evbd lit
                     end
@@ -1858,7 +1858,7 @@ let destructure_goal gl =
           (tclTHEN 
 	     (tclTHEN
 		(Tactics.refine 
-		   (mkAppL (Lazy.force coq_dec_not_not, [| t;
+		   (mkApp (Lazy.force coq_dec_not_not, [| t;
 			      decidability gl t; mkNewMeta () |])))
 		intro) 
 	     (destructure_hyps))