Renommage AppL en App

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

6 files changed, 117 insertions, 117 deletions

diff --git a/contrib/omega/coq_omega.ml b/contrib/omega/coq_omega.ml
index 963f41821..06c404aef 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)) 
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index f16b6049e..a3dd19dd6 100644
--- a/contrib/ring/quote.ml
+++ b/contrib/ring/quote.ml
@@ -189,7 +189,7 @@ let compute_lhs typ i nargsi =
   match kind_of_term typ with
     | IsMutInd((sp,0),args) -> 
         let argsi = Array.init nargsi (fun j -> mkMeta (nargsi - j)) in
-        mkAppL (mkMutConstruct (((sp,0),i+1), args), argsi)
+        mkApp (mkMutConstruct (((sp,0),i+1), args), argsi)
     | _ -> i_can't_do_that ()
 
 (*s This function builds the pattern from the RHS. Recursive calls are
@@ -198,10 +198,10 @@ let compute_lhs typ i nargsi =
 let compute_rhs bodyi index_of_f =
   let rec aux c = 
     match decomp_term c with
-      | IsAppL (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
+      | IsApp (j, args) when j = mkRel (index_of_f) (* recursive call *) -> 
           let i = destRel (array_last args) in mkMeta i
-      | IsAppL (f,args) ->
-          mkAppL (f, Array.map aux args)
+      | IsApp (f,args) ->
+          mkApp (f, Array.map aux args)
       | IsCast (c,t) -> aux c 
       | _ -> c
   in
@@ -282,7 +282,7 @@ let rec closed_under cset t =
   (ConstrSet.mem t cset) or
   (match (kind_of_term t) with
      | IsCast(c,_) -> closed_under cset c  
-     | IsAppL(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
+     | IsApp(f,l) -> closed_under cset f & array_for_all (closed_under cset) l
      | _ -> false)
     
 (*s [btree_of_array [| c1; c2; c3; c4; c5 |]] builds the complete
@@ -303,13 +303,13 @@ let btree_of_array a ty =
   let size_of_a = Array.length a in
   let semi_size_of_a = size_of_a lsr 1 in
   let node = Lazy.force coq_Node_vm  
-  and empty = mkAppL (Lazy.force coq_Empty_vm, [| ty |]) in
+  and empty = mkApp (Lazy.force coq_Empty_vm, [| ty |]) in
   let rec aux n =
     if n > size_of_a 
     then empty
     else if  n > semi_size_of_a 
-    then mkAppL (node, [| ty; a.(n-1); empty; empty |])
-    else mkAppL (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |])
+    then mkApp (node, [| ty; a.(n-1); empty; empty |])
+    else mkApp (node, [| ty; a.(n-1); aux (2*n); aux (2*n+1) |])
   in 
   aux 1
 
@@ -326,7 +326,7 @@ let path_of_int n =
     else (n mod 2 = 1)::(digits_of_int (n lsr 1))
   in
   List.fold_right 
-    (fun b c -> mkAppL ((if b then Lazy.force coq_Right_idx 
+    (fun b c -> mkApp ((if b then Lazy.force coq_Right_idx 
                          else Lazy.force coq_Left_idx),
                          [| c |]))
     (List.rev (digits_of_int n))
@@ -343,7 +343,7 @@ let path_of_int n =
 let rec subterm gl (t : constr) (t' : constr) = 
   (pf_conv_x gl t t') or
   (match (kind_of_term t) with 
-     | IsAppL (f,args) -> array_exists (fun t -> subterm gl t t') args
+     | IsApp (f,args) -> array_exists (fun t -> subterm gl t t') args
      | IsCast(t,_) -> (subterm gl t t')
      | _ -> false)
            
@@ -428,8 +428,8 @@ let quote f lid gl =
     | _ -> assert false
   in
   match ivs.variable_lhs with
-    | None -> Tactics.convert_concl (mkAppL (f, [| p |])) gl
-    | Some _ -> Tactics.convert_concl (mkAppL (f, [| vm; p |])) gl
+    | None -> Tactics.convert_concl (mkApp (f, [| p |])) gl
+    | Some _ -> Tactics.convert_concl (mkApp (f, [| vm; p |])) gl
 
 (*i*)
 let dyn_quote = function
diff --git a/contrib/ring/ring.ml b/contrib/ring/ring.ml
index 7c514bd2a..d2064380b 100644
--- a/contrib/ring/ring.ml
+++ b/contrib/ring/ring.ml
@@ -173,12 +173,12 @@ let add_theory want_ring want_abstract a aplus amult aone azero aopp aeq t cset
   let env = Global.env () in
   if (want_ring & 
       not (is_conv env Evd.empty (Typing.type_of env Evd.empty t)
-	     (mkAppL (Lazy.force coq_Ring_Theory, [| a; aplus; amult;
+	     (mkApp (Lazy.force coq_Ring_Theory, [| a; aplus; amult;
 			aone; azero; aopp; aeq |])))) then
     errorlabstrm "addring" [< 'sTR "Not a valid Ring theory" >];
   if (not want_ring &
       not (is_conv  env Evd.empty (Typing.type_of env Evd.empty t) 
-	     (mkAppL (Lazy.force coq_Semi_Ring_Theory, [| a; 
+	     (mkApp (Lazy.force coq_Semi_Ring_Theory, [| a; 
 			aplus; amult; aone; azero; aeq |])))) then 
     errorlabstrm "addring" [< 'sTR "Not a valid Semi-Ring theory" >];
   Lib.add_anonymous_leaf
@@ -300,9 +300,9 @@ let build_spolynom gl th lc =
      and builds the varmap with side-effects *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsAppL (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+      | IsApp (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_SPplus; th.th_a; aux c1; aux c2 |]
-      | IsAppL (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+      | IsApp (binop,[|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
 	  mkAppA [| Lazy.force coq_SPmult; th.th_a; aux c1; aux c2 |]
       | _ when closed_under th.th_closed c ->
 	  mkAppA [| Lazy.force coq_SPconst; th.th_a; c |]
@@ -354,17 +354,17 @@ let build_polynom gl th lc =
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1; aux c2 |]
-      | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
 	  mkAppA [| Lazy.force coq_Pmult; th.th_a; aux c1; aux c2 |]
       (* The special case of Zminus *)
-      | IsAppL (binop, [|c1; c2|])
+      | IsApp (binop, [|c1; c2|])
 	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
 	                                 mkAppA [| th.th_opp; c2 |] |]) ->
 	    mkAppA [| Lazy.force coq_Pplus; th.th_a; aux c1;
 	              mkAppA [| Lazy.force coq_Popp; th.th_a; aux c2 |] |]
-      | IsAppL (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
+      | IsApp (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
 	  mkAppA [| Lazy.force coq_Popp; th.th_a; aux c1 |]
       | _ when closed_under th.th_closed c ->
 	  mkAppA [| Lazy.force coq_Pconst; th.th_a; c |]
@@ -419,9 +419,9 @@ let build_aspolynom gl th lc =
      and builds the varmap with side-effects *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_ASPplus; aux c1; aux c2 |]
-      | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
 	  mkAppA [| Lazy.force coq_ASPmult; aux c1; aux c2 |]
       | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_ASP0
       | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_ASP1
@@ -470,17 +470,17 @@ let build_apolynom gl th lc =
   let counter = ref 1 in (* number of variables created + 1 *)
   let rec aux c = 
     match (kind_of_term (strip_outer_cast c)) with 
-      | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_plus ->
 	  mkAppA [| Lazy.force coq_APplus; aux c1; aux c2 |]
-      | IsAppL (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
+      | IsApp (binop, [|c1; c2|]) when pf_conv_x gl binop th.th_mult ->
 	  mkAppA [| Lazy.force coq_APmult; aux c1; aux c2 |]
       (* The special case of Zminus *)
-      | IsAppL (binop, [|c1; c2|]) 
+      | IsApp (binop, [|c1; c2|]) 
 	  when pf_conv_x gl c (mkAppA [| th.th_plus; c1; 
 	                                 mkAppA [| th.th_opp; c2 |] |]) ->
 	    mkAppA [| Lazy.force coq_APplus; aux c1;
 	              mkAppA [| Lazy.force coq_APopp; aux c2 |] |]
-      | IsAppL (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
+      | IsApp (unop, [|c1|]) when pf_conv_x gl unop th.th_opp ->
 	  mkAppA [| Lazy.force coq_APopp; aux c1 |]
       | _ when pf_conv_x gl c th.th_zero -> Lazy.force coq_AP0
       | _ when pf_conv_x gl c th.th_one -> Lazy.force coq_AP1
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index d7b2306cc..12e8ed33b 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -90,7 +90,7 @@ let constr_display csr =
   | IsLetIn (na,b,t,c) ->
       "LetIn("^(name_display na)^","^(term_display b)^","
       ^(term_display t)^","^(term_display c)^")"
-  | IsAppL (c,l) -> "App("^(term_display c)^","^(array_display l)^")"
+  | IsApp (c,l) -> "App("^(term_display c)^","^(array_display l)^")"
   | IsEvar (e,l) -> "Evar("^(string_of_int e)^","^(array_display l)^")"
   | IsConst (c,l) -> "Const("^(string_of_path c)^","^(array_display l)^")"
   | IsMutInd ((sp,i),l) ->
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 14381b7d7..1fd4fc403 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -223,7 +223,7 @@ let build_recursive lnameargsardef =
     with e ->
       States.unfreeze fs; raise e
   in 
-  let recdef = 
+  let recdef = (* TODO: remplacer mkCast par un appel à interp_casted_constr *)
     try 
       List.map (fun (_,lparams,arityc,def) -> 
                   interp_constr sigma rec_sign 
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 477a294b8..dc6f01d34 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -201,7 +201,7 @@ let expmod_constr oldenv modlist c =
     | IsCast (c,t) -> mkCast (f c,f t)
     | _ -> f c 
   in
-  let c' = modify_opers expfun (fun a b -> mkAppL (a, [|b|])) modlist c in
+  let c' = modify_opers expfun (fun a b -> mkApp (a, [|b|])) modlist c in
   match kind_of_term c' with
     | IsCast (val_0,typ) -> mkCast (simpfun val_0,simpfun typ)
     | _ -> simpfun c'