Renommage AppL en App

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

7 files changed, 83 insertions, 89 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 0bb893c6f7..f18d7e0776 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -388,7 +388,7 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
   subst_bodies_from_i 0 env, bds.(i)
 
 
-(* type of terms with a hole. This hole can appear only under AppL or Case.
+(* type of terms with a hole. This hole can appear only under App or Case.
  *   TOP means the term is considered without context
  *   APP(l,stk) means the term is applied to l, and then we have the context st
  *      this corresponds to the application stack of the KAM.
@@ -499,7 +499,7 @@ let rec norm_head info env t stack =
   (* no reduction under binders *)
   match kind_of_term t with
   (* stack grows (remove casts) *)
-  | IsAppL (head,args) -> (* Applied terms are normalized immediately;
+  | IsApp (head,args) -> (* Applied terms are normalized immediately;
                         they could be computed when getting out of the stack *)
       let nargs = Array.map (cbv_stack_term info TOP env) args in
       norm_head info env head (stack_app (Array.to_list nargs) stack)
@@ -810,7 +810,7 @@ let rec traverse_term env t =
     | IsCast (a,b) ->
         { norm = false;
           term = FCast (traverse_term env a, traverse_term env b)}
-    | IsAppL (f,v) ->
+    | IsApp (f,v) ->
         { norm = false;
 	  term = FApp (traverse_term env f, Array.map (traverse_term env) v) }
     | IsMutInd (sp,v) ->
@@ -889,7 +889,7 @@ let rec lift_term_of_freeze lfts v =
 	mkCoFix (op, (Array.map (lift_term_of_freeze lfts) tys, lna,
 		      Array.map (lift_term_of_freeze lfts') bds))
     | FApp (f,ve) ->
-	mkAppL (lift_term_of_freeze lfts f,
+	mkApp (lift_term_of_freeze lfts f,
 		Array.map (lift_term_of_freeze lfts) ve)
     | FLambda (n,t,c,_,_)   ->
 	mkLambda (n, lift_term_of_freeze lfts t, 
@@ -945,7 +945,7 @@ let rec fstrong unfreeze_fun lfts v =
 	mkCoFix (op, (Array.map (fstrong unfreeze_fun lfts) tys, lna,
 		      Array.map (fstrong unfreeze_fun lfts') bds))
     | FApp (f,ve) ->
-	mkAppL (fstrong unfreeze_fun lfts f,
+	mkApp (fstrong unfreeze_fun lfts f,
 		Array.map (fstrong unfreeze_fun lfts) ve)
     | FLambda (n,t,c,_,_)   ->
 	mkLambda (n, fstrong unfreeze_fun lfts t,
@@ -1172,7 +1172,7 @@ and whnf_term info env t =
     | IsSort _ | IsXtra _ | IsMeta _ -> {norm = true; term = FAtom t }
     | IsCast (c,_) -> whnf_term info env c    (* remove outer casts *)
 
-    | IsAppL (f,ve) ->
+    | IsApp (f,ve) ->
       	whnf_frterm info
 	  { norm = false; term = FApp (freeze env f, freeze_vect env ve)}
     | IsConst (op,ve) ->
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 456e89bad9..100db950f0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -216,7 +216,7 @@ let hdchar env c =
     | IsLambda (_,_,c)     -> hdrec (k+1) c
     | IsLetIn (_,_,_,c)    -> hdrec (k+1) c
     | IsCast (c,_)         -> hdrec k c
-    | IsAppL (f,l)         -> hdrec k f
+    | IsApp (f,l)         -> hdrec k f
     | IsConst (sp,_)       ->
 	let c = lowercase_first_char (basename sp) in
 	if c = "?" then "y" else c
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 84b5b7a076..827956fd5f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -98,7 +98,7 @@ let append_stack v s = v@s
 
 let rec whd_state (x, stack as s) =
   match kind_of_term x with
-    | IsAppL (f,cl) -> whd_state (f, append_stack cl stack)
+    | IsApp (f,cl) -> whd_state (f, append_stack cl stack)
     | IsCast (c,_)  -> whd_state (c, stack)
     | _             -> s
 
@@ -278,13 +278,13 @@ let whd_state_gen flags env sigma =
 	     | None -> s)
       | IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
-      | IsAppL (f,cl)  -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | Some (a,m) when red_beta flags -> stacklam whrec [a] c m
              | None when red_eta flags ->
                  (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
-                    | IsAppL (f,cl) ->
+                    | IsApp (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
 			  let x', l' = whrec (array_last cl, empty_stack) in
@@ -321,13 +321,13 @@ let local_whd_state_gen flags =
     match kind_of_term x with
       | IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
-      | IsAppL (f,cl)  -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl)  -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | Some (a,m) when red_beta flags -> stacklam whrec [a] c m
              | None when red_eta flags ->
                  (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
-                    | IsAppL (f,cl) ->
+                    | IsApp (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
 			  let x', l' = whrec (array_last cl, empty_stack) in
@@ -370,7 +370,7 @@ let whd_beta_state =
 	     | Some (a1,rest) -> stacklam whrec [a1] c2 rest)
 
       | IsCast (c,_) -> whrec (c, stack)
-      | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl) -> whrec (f, append_stack cl stack)
       | x -> s
   in
   whrec
@@ -392,7 +392,7 @@ let whd_delta_state env sigma =
           whrec (existential_value sigma (ev,args), l)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
       | IsCast (c,_) -> whrec (c, l)
-      | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+      | IsApp (f,cl) -> whrec (f, append_stack cl l)
       | x -> s
   in 
   whrec
@@ -420,7 +420,7 @@ let whd_betadelta_state env sigma =
 	    s
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
       | IsCast (c,_) -> whrec (c, l)
-      | IsAppL (f,cl)  -> whrec (f, append_stack cl l)
+      | IsApp (f,cl)  -> whrec (f, append_stack cl l)
       | IsLambda (_,_,c) ->
           (match decomp_stack l with
              | None -> s
@@ -447,7 +447,7 @@ let whd_betaevar_stack env sigma =
           else 
 	    s
       | IsCast (c,_) -> whrec (c, l)
-      | IsAppL (f,cl)  -> whrec (f, append_stack cl l)
+      | IsApp (f,cl)  -> whrec (f, append_stack cl l)
       | IsLambda (_,_,c) ->
           (match decomp_stack l with
              | None -> s
@@ -473,12 +473,12 @@ let whd_betadeltaeta_state env sigma =
 	  whrec (existential_value sigma (ev,args), l)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
       | IsCast (c,_) -> whrec (c, l)
-      | IsAppL (f,cl)  -> whrec (f, append_stack cl l)
+      | IsApp (f,cl)  -> whrec (f, append_stack cl l)
       | IsLambda (_,_,c) ->
           (match decomp_stack l with
              | None ->
                  (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
-                    | IsAppL (f,cl) ->
+                    | IsApp (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
 			  let x',l' = whrec (array_last cl, empty_stack) in
@@ -514,7 +514,7 @@ let whd_betaiota_state =
   let rec whrec (x,stack as s) =
     match kind_of_term x with
       | IsCast (c,_)     -> whrec (c, stack)
-      | IsAppL (f,cl)    -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | None -> s
@@ -553,7 +553,7 @@ let whd_betaiotaevar_state env sigma =
           else 
 	    s
       | IsCast (c,_) -> whrec (c, stack)
-      | IsAppL (f,cl)    -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | None -> s
@@ -591,7 +591,7 @@ let whd_betadeltaiota_state env sigma =
 	  whrec (existential_value sigma (ev,args), stack)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
-      | IsAppL (f,cl)    -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | None -> s
@@ -629,12 +629,12 @@ let whd_betadeltaiotaeta_state env sigma =
 	  whrec (existential_value sigma (ev,args), stack)
       | IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
       | IsCast (c,_) -> whrec (c, stack)
-      | IsAppL (f,cl)    -> whrec (f, append_stack cl stack)
+      | IsApp (f,cl)    -> whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
              | None ->
                  (match kind_of_term (app_stack (whrec (c, empty_stack))) with 
-                    | IsAppL (f,cl) ->
+                    | IsApp (f,cl) ->
 			let napp = Array.length cl in
 			if napp > 0 then
 			  let x', l' = whrec (array_last cl, empty_stack) in
@@ -1062,7 +1062,7 @@ let hnf env sigma c = apprec env sigma (c, empty_stack)
 let whd_programs_stack env sigma = 
   let rec whrec (x, stack as s) =
     match kind_of_term x with
-      | IsAppL (f,([|c|] as cl)) ->
+      | IsApp (f,([|c|] as cl)) ->
 	  if occur_meta c then s else whrec (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5c1493e2a8..f1b97bcd22 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -92,7 +92,7 @@ let rec execute mf env cstr =
     | IsSort (Type u) ->
 	judge_of_type u
 	  
-    | IsAppL (f,args) ->
+    | IsApp (f,args) ->
 	let (j,cst1) = execute mf env f in
         let (jl,cst2) = execute_array mf env args in
 	let (j,cst3) =
diff --git a/kernel/term.ml b/kernel/term.ml
index 38e3f5bfe1..9829c1154f 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -67,7 +67,7 @@ type kind_of_term =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsLetIn        of name * constr * constr * constr
-  | IsAppL         of constr * constr array
+  | IsApp         of constr * constr array
   | IsEvar         of existential
   | IsConst        of constant
   | IsMutInd       of inductive
@@ -85,7 +85,7 @@ val mkCast : constr * constr -> constr
 val mkProd : name * constr * constr -> constr
 val mkLambda : name * constr * constr -> constr
 val mkLetIn : name * constr * constr * constr -> constr
-val mkAppL : constr * constr array -> constr
+val mkApp : constr * constr array -> constr
 val mkEvar : existential -> constr
 val mkConst : constant -> constr
 val mkMutInd : inductive -> constr
@@ -129,7 +129,7 @@ and kind_of_term =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsLetIn        of name * constr * constr * constr
-  | IsAppL         of constr * constr array
+  | IsApp         of constr * constr array
   | IsEvar         of existential
   | IsConst        of constant
   | IsMutInd       of inductive
@@ -154,7 +154,7 @@ let comp_term t1 t2 =
   | IsLambda (n1,t1,c1), IsLambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
   | IsLetIn (n1,b1,t1,c1), IsLetIn (n2,b2,t2,c2) ->
       n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
-  | IsAppL (c1,l1), IsAppL (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
+  | IsApp (c1,l1), IsApp (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
   | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 (==) l1 l2
   | IsConst (c1,l1), IsConst (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
   | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
@@ -180,7 +180,7 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t =
   | IsProd (na,t,c) -> IsProd (sh_na na, sh_rec t, sh_rec c)
   | IsLambda (na,t,c) -> IsLambda (sh_na na, sh_rec t, sh_rec c)
   | IsLetIn (na,b,t,c) -> IsLetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
-  | IsAppL (c,l) -> IsAppL (sh_rec c, Array.map sh_rec l)
+  | IsApp (c,l) -> IsApp (sh_rec c, Array.map sh_rec l)
   | IsEvar (e,l) -> IsEvar (e, Array.map sh_rec l)
   | IsConst (c,l) -> IsConst (sh_sp c, Array.map sh_rec l)
   | IsMutInd ((sp,i),l) -> IsMutInd ((sh_sp sp,i), Array.map sh_rec l)
@@ -242,11 +242,11 @@ let mkLetIn (x,c1,t,c2) = IsLetIn (x,c1,t,c2)
 (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
 (* We ensure applicative terms have at most one arguments and the
    function is not itself an applicative term *)
-let mkAppL (f, a) = 
+let mkApp (f, a) = 
   if a=[||] then f else
     match f with
-      | IsAppL (g, cl) -> IsAppL (g, Array.append cl a)
-      | _ -> IsAppL (f, a)
+      | IsApp (g, cl) -> IsApp (g, Array.append cl a)
+      | _ -> IsApp (f, a)
 
 
 (* Constructs a constant *) 
@@ -297,7 +297,7 @@ open Internal
 
 END of expected re-export of Internal module *)
 
-(* User view of [constr]. For [IsAppL], it is ensured there is at
+(* User view of [constr]. For [IsApp], it is ensured there is at
    least one argument and the function is not itself an applicative
    term *)
 
@@ -420,10 +420,10 @@ let destLetIn c = match kind_of_term c with
 
 (* Destructs an application *)
 let destApplication c = match kind_of_term c with
-  | IsAppL (f,a) -> (f, a)
+  | IsApp (f,a) -> (f, a)
   | _ -> invalid_arg "destApplication"
 
-let isAppL c = match kind_of_term c with IsAppL _ -> true | _ -> false
+let isApp c = match kind_of_term c with IsApp _ -> true | _ -> false
 
 (* Destructs a constant *)
 let destConst c = match kind_of_term c with
@@ -505,7 +505,7 @@ let fold_constr f acc c = match kind_of_term c with
   | IsProd (_,t,c) -> f (f acc t) c
   | IsLambda (_,t,c) -> f (f acc t) c
   | IsLetIn (_,b,t,c) -> f (f (f acc b) t) c
-  | IsAppL (c,l) -> Array.fold_left f (f acc c) l
+  | IsApp (c,l) -> Array.fold_left f (f acc c) l
   | IsEvar (_,l) -> Array.fold_left f acc l
   | IsConst (_,l) -> Array.fold_left f acc l
   | IsMutInd (_,l) -> Array.fold_left f acc l
@@ -529,7 +529,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
   | IsProd (_,t,c) -> f (g n) (f n acc t) c
   | IsLambda (_,t,c) -> f (g n) (f n acc t) c
   | IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
-  | IsAppL (c,l) -> Array.fold_left (f n) (f n acc c) l
+  | IsApp (c,l) -> Array.fold_left (f n) (f n acc c) l
   | IsEvar (_,l) -> Array.fold_left (f n) acc l
   | IsConst (_,l) -> Array.fold_left (f n) acc l
   | IsMutInd (_,l) -> Array.fold_left (f n) acc l
@@ -552,7 +552,7 @@ let iter_constr f c = match kind_of_term c with
   | IsProd (_,t,c) -> f t; f c
   | IsLambda (_,t,c) -> f t; f c
   | IsLetIn (_,b,t,c) -> f b; f t; f c
-  | IsAppL (c,l) -> f c; Array.iter f l
+  | IsApp (c,l) -> f c; Array.iter f l
   | IsEvar (_,l) -> Array.iter f l
   | IsConst (_,l) -> Array.iter f l
   | IsMutInd (_,l) -> Array.iter f l
@@ -573,7 +573,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
   | IsProd (_,t,c) -> f n t; f (g n) c
   | IsLambda (_,t,c) -> f n t; f (g n) c
   | IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c
-  | IsAppL (c,l) -> f n c; Array.iter (f n) l
+  | IsApp (c,l) -> f n c; Array.iter (f n) l
   | IsEvar (_,l) -> Array.iter (f n) l
   | IsConst (_,l) -> Array.iter (f n) l
   | IsMutInd (_,l) -> Array.iter (f n) l
@@ -594,7 +594,7 @@ let map_constr f c = match kind_of_term c with
   | IsProd (na,t,c) -> mkProd (na, f t, f c)
   | IsLambda (na,t,c) -> mkLambda (na, f t, f c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
-  | IsAppL (c,l) -> mkAppL (f c, Array.map f l)
+  | IsApp (c,l) -> mkApp (f c, Array.map f l)
   | IsEvar (e,l) -> mkEvar (e, Array.map f l)
   | IsConst (c,l) -> mkConst (c, Array.map f l)
   | IsMutInd (c,l) -> mkMutInd (c, Array.map f l)
@@ -615,7 +615,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
-  | IsAppL (c,al) -> mkAppL (f l c, Array.map (f l) al)
+  | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
   | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
   | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
   | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
@@ -640,7 +640,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
   | IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c)
   | IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
   | IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
-  | IsAppL (c,al) -> mkAppL (f l c, Array.map (f l) al)
+  | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
   | IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
   | IsConst (c,al) -> mkConst (c, Array.map (f l) al)
   | IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
@@ -693,8 +693,8 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
   | IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c)
   | IsLetIn (na,b,t,c) ->
       let b' = f l b in let t' = f l t in mkLetIn (na, b', t', f (g l) c)
-  | IsAppL (c,al) -> 
-      let c' = f l c in mkAppL (c', array_map_left (f l) al)
+  | IsApp (c,al) -> 
+      let c' = f l c in mkApp (c', array_map_left (f l) al)
   | IsEvar (e,al) -> mkEvar (e, array_map_left (f l) al)
   | IsConst (c,al) -> mkConst (c, array_map_left (f l) al)
   | IsMutInd (c,al) -> mkMutInd (c, array_map_left (f l) al)
@@ -727,7 +727,7 @@ let compare_constr f c1 c2 =
   | IsProd (_,t1,c1), IsProd (_,t2,c2) -> f t1 t2 & f c1 c2
   | IsLambda (_,t1,c1), IsLambda (_,t2,c2) -> f t1 t2 & f c1 c2
   | IsLetIn (_,b1,t1,c1), IsLetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
-  | IsAppL (c1,l1), IsAppL (c2,l2) -> f c1 c2 & array_for_all2 f l1 l2
+  | IsApp (c1,l1), IsApp (c2,l2) -> f c1 c2 & array_for_all2 f l1 l2
   | IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
   | IsConst (c1,l1), IsConst (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
   | IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
@@ -850,7 +850,7 @@ let noccur_between n m term =
 let noccur_with_meta n m term = 
   let rec occur_rec n c = match kind_of_term c with
     | IsRel p -> if n<=p & p<n+m then raise Occur
-    | IsAppL(f,cl) ->
+    | IsApp(f,cl) ->
 	(match kind_of_term f with
            | IsCast (c,_) when isMeta c -> ()
            | IsMeta _ -> ()
@@ -1072,16 +1072,12 @@ let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
 (* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
 (* We ensure applicative terms have at most one arguments and the
    function is not itself an applicative term *)
-let mkAppL = mkAppL
-
-let mkAppList = function
-  | f::l -> mkAppL (f, Array.of_list l)
-  | _ -> anomaly "mkAppList received an empty list"
+let mkApp = mkApp
 
 let mkAppA v =
   let l = Array.length v in
   if l=0 then anomaly "mkAppA received an empty array"
-  else mkAppL (v.(0), Array.sub v 1 (Array.length v -1))
+  else mkApp (v.(0), Array.sub v 1 (Array.length v -1))
 
 (* Constructs a constant *) 
 (* The array of terms correspond to the variables introduced in the section *)
@@ -1190,13 +1186,13 @@ let lamn n env b =
   in 
   lamrec (n,env,b)
 
-let applist (f,l) = mkAppL (f, Array.of_list l)
+let applist (f,l) = mkApp (f, Array.of_list l)
 
-let applistc f l = mkAppL (f, Array.of_list l)
+let applistc f l = mkApp (f, Array.of_list l)
 
-let appvect = mkAppL
+let appvect = mkApp
 	    
-let appvectc f l = mkAppL (f,l)
+let appvectc f l = mkApp (f,l)
 		     
 (* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
  * [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
@@ -1350,28 +1346,28 @@ let le_kind_implicit k1 k2 =
 
 (* flattens application lists *)
 let rec collapse_appl c = match kind_of_term c with
-  | IsAppL (f,cl) -> 
+  | IsApp (f,cl) -> 
       let rec collapse_rec f cl2 = match kind_of_term f with
-	| IsAppL (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
-	| IsCast (c,_) when isAppL c -> collapse_rec c cl2
-	| _ -> if cl2 = [||] then f else mkAppL (f,cl2)
+	| IsApp (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+	| IsCast (c,_) when isApp c -> collapse_rec c cl2
+	| _ -> if cl2 = [||] then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
   | _ -> c
 
 let rec decomp_app c =
   match kind_of_term (collapse_appl c) with
-    | IsAppL (f,cl) -> (f, Array.to_list cl)
+    | IsApp (f,cl) -> (f, Array.to_list cl)
     | IsCast (c,t) -> decomp_app c
     | _ -> (c,[])
 
 (* strips head casts and flattens head applications *)
 let rec strip_head_cast c = match kind_of_term c with
-  | IsAppL (f,cl) -> 
+  | IsApp (f,cl) -> 
       let rec collapse_rec f cl2 = match kind_of_term f with
-	| IsAppL (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+	| IsApp (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
 	| IsCast (c,_) -> collapse_rec c cl2
-	| _ -> if cl2 = [||] then f else mkAppL (f,cl2)
+	| _ -> if cl2 = [||] then f else mkApp (f,cl2)
       in 
       collapse_rec f cl
   | IsCast (c,t) -> strip_head_cast c
@@ -1458,7 +1454,7 @@ let rec eta_reduce_head c =
   match kind_of_term c with
     | IsLambda (_,c1,c') ->
 	(match kind_of_term (eta_reduce_head c') with
-           | IsAppL (f,cl) ->
+           | IsApp (f,cl) ->
                let lastn = (Array.length cl) - 1 in 
                if lastn < 1 then anomaly "application without arguments"
                else
@@ -1466,7 +1462,7 @@ let rec eta_reduce_head c =
                     | IsRel 1 ->
 			let c' =
                           if lastn = 1 then f
-			  else mkAppL (f, Array.sub cl 0 lastn)
+			  else mkApp (f, Array.sub cl 0 lastn)
 			in
 			if not (dependent (mkRel 1) c')
                         then lift (-1) c'
@@ -1510,12 +1506,12 @@ let rec rename_bound_var l c =
 let prefix_application (k,c) (t : constr) = 
   let c' = strip_head_cast c and t' = strip_head_cast t in
   match kind_of_term c', kind_of_term t' with
-    | IsAppL (f1,cl1), IsAppL (f2,cl2) ->
+    | IsApp (f1,cl1), IsApp (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2
-	   && eq_constr c' (mkAppL (f2, Array.sub cl2 0 l1)) then
-	  Some (mkAppL (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+	   && eq_constr c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else 
 	  None
     | _ -> None
@@ -1523,12 +1519,12 @@ let prefix_application (k,c) (t : constr) =
 let prefix_application_eta (k,c) (t : constr) =
   let c' = strip_head_cast c and t' = strip_head_cast t in
   match kind_of_term c', kind_of_term t' with
-    | IsAppL (f1,cl1), IsAppL (f2,cl2) ->
+    | IsApp (f1,cl1), IsApp (f2,cl2) ->
 	let l1 = Array.length cl1
 	and l2 = Array.length cl2 in
 	if l1 <= l2 &&
-           eta_eq_constr  c' (mkAppL (f2, Array.sub cl2 0 l1)) then
-	  Some (mkAppL (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+           eta_eq_constr  c' (mkApp (f2, Array.sub cl2 0 l1)) then
+	  Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
 	else 
 	  None
   | (_,_) -> None
@@ -1700,7 +1696,7 @@ type constr_operator =
   | OpSort of sorts
   | OpRel of int | OpVar of identifier
   | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
-  | OpAppL | OpConst of section_path
+  | OpApp | OpConst of section_path
   | OpEvar of existential_key
   | OpMutInd of inductive_path
   | OpMutConstruct of constructor_path
@@ -1717,7 +1713,7 @@ let splay_constr c = match kind_of_term c with
   | IsProd (x, t1, t2)         -> OpProd x, [|t1;t2|]
   | IsLambda (x, t1, t2)       -> OpLambda x, [|t1;t2|]
   | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [|b;t1;t2|]
-  | IsAppL (f,a)               -> OpAppL, Array.append [|f|] a
+  | IsApp (f,a)               -> OpApp, Array.append [|f|] a
   | IsConst (sp, a)            -> OpConst sp, a
   | IsEvar (sp, a)             -> OpEvar sp, a
   | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, l
@@ -1736,7 +1732,7 @@ let gather_constr = function
   | OpProd x, [|t1;t2|]   -> mkProd (x, t1, t2)
   | OpLambda x, [|t1;t2|] -> mkLambda (x, t1, t2)
   | OpLetIn x, [|b;t1;t2|] -> mkLetIn (x, b, t1, t2)
-  | OpAppL, v     -> let f = v.(0) and a = array_tl v in mkAppL (f, a)
+  | OpApp, v     -> let f = v.(0) and a = array_tl v in mkApp (f, a)
   | OpConst sp, a -> mkConst (sp, a)
   | OpEvar sp, a  -> mkEvar (sp, a) 
   | OpMutInd ind_sp, l        -> mkMutInd (ind_sp, l) 
@@ -1772,7 +1768,7 @@ let splay_constr_with_binders c = match kind_of_term c with
   | IsProd (x, t1, t2)         -> OpProd x, [x,None,t1], [|t2|]
   | IsLambda (x, t1, t2)       -> OpLambda x, [x,None,t1], [|t2|]
   | IsLetIn (x, b, t1, t2)     -> OpLetIn x, [x,Some b,t1], [|t2|]
-  | IsAppL (f,v)               -> OpAppL, [], Array.append [|f|] v
+  | IsApp (f,v)               -> OpApp, [], Array.append [|f|] v
   | IsConst (sp, a)            -> OpConst sp, [], a
   | IsEvar (sp, a)             -> OpEvar sp, [], a
   | IsMutInd (ind_sp, l)       -> OpMutInd ind_sp, [], l
@@ -1802,7 +1798,7 @@ let gather_constr_with_binders = function
   | OpProd _, [x,None,t1], [|t2|]   -> mkProd (x, t1, t2)
   | OpLambda _, [x,None,t1], [|t2|] -> mkLambda (x, t1, t2)
   | OpLetIn _, [x,Some b,t1], [|t2|] -> mkLetIn (x, b, t1, t2)
-  | OpAppL, [], v     -> let f = v.(0) and a = array_tl v in mkAppL (f, a)
+  | OpApp, [], v     -> let f = v.(0) and a = array_tl v in mkApp (f, a)
   | OpConst sp, [], a -> mkConst (sp, a)
   | OpEvar sp, [], a  -> mkEvar (sp, a) 
   | OpMutInd ind_sp, [], l        -> mkMutInd (ind_sp, l) 
diff --git a/kernel/term.mli b/kernel/term.mli
index 1994584af6..fe26462dec 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -116,7 +116,7 @@ type kind_of_term =
   | IsProd         of name * constr * constr
   | IsLambda       of name * constr * constr
   | IsLetIn        of name * constr * constr * constr
-  | IsAppL         of constr * constr array
+  | IsApp         of constr * constr array
   | IsEvar         of existential
   | IsConst        of constant
   | IsMutInd       of inductive
@@ -125,7 +125,7 @@ type kind_of_term =
   | IsFix          of fixpoint
   | IsCoFix        of cofixpoint
 
-(* User view of [constr]. For [IsAppL], it is ensured there is at
+(* User view of [constr]. For [IsApp], it is ensured there is at
    least one argument and the function is not itself an applicative
    term *)
 
@@ -197,10 +197,9 @@ val mkNamedLambda : identifier -> constr -> constr -> constr
 (* [mkLambda_string s t c] constructs $[s:t]c$ *)
 val mkLambda_string : string -> constr -> constr -> constr
 
-(* [mkAppL (f,[| t_1; ...; t_n |]] constructs the application
+(* [mkApp (f,[| t_1; ...; t_n |]] constructs the application
    $(f~t_1~\dots~t_n)$. *)
-val mkAppL : constr * constr array -> constr
-val mkAppList : constr list  -> constr
+val mkApp : constr * constr array -> constr
 val mkAppA : constr array -> constr
 
 (* Constructs a constant *) 
@@ -317,7 +316,7 @@ val destLambda : constr -> name * constr * constr
 val destLetIn : constr -> name * constr * constr * constr
 
 (* Destructs an application *)
-val isAppL : constr -> bool
+val isApp : constr -> bool
 (*i
 val hd_app : constr -> constr 
 val args_app : constr -> constr array
@@ -365,8 +364,7 @@ val abs_implicit : constr -> constr
 val lambda_implicit : constr -> constr
 val lambda_implicit_lift : int -> constr -> constr
 
-(* [applist (f,args)] and co build [mkAppL (f,args)] if [args] non
-   empty and build [f] otherwise *)
+(* [applist (f,args)] and co work as [mkApp] *)
 
 val applist : constr * constr list -> constr
 val applistc : constr -> constr list -> constr
@@ -561,7 +559,7 @@ type constr_operator =
   | OpSort of sorts
   | OpRel of int | OpVar of identifier
   | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
-  | OpAppL | OpConst of section_path
+  | OpApp | OpConst of section_path
   | OpEvar of existential_key
   | OpMutInd of inductive_path
   | OpMutConstruct of constructor_path
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c4e177d44e..74b207209d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -616,7 +616,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
 	    (array_for_all (check_rec_call n lst) la) &&
             (List.for_all (check_rec_call n lst) l)
 
-	| IsAppL (f,la) -> 
+	| IsApp (f,la) -> 
 	    (check_rec_call n lst f) &&
 	    (array_for_all (check_rec_call n lst) la) &&
             (List.for_all (check_rec_call n lst) l)
@@ -831,7 +831,7 @@ let control_only_guard env sigma =
     | IsMutConstruct (_,cl) -> Array.iter control_rec cl
     | IsConst (_,cl)        -> Array.iter control_rec cl
     | IsEvar (_,cl)         -> Array.iter control_rec cl
-    | IsAppL (_,cl)         -> Array.iter control_rec cl
+    | IsApp (_,cl)         -> Array.iter control_rec cl
     | IsCast (c1,c2)       -> control_rec c1; control_rec c2
     | IsProd (_,c1,c2)     -> control_rec c1; control_rec c2
     | IsLambda (_,c1,c2)   -> control_rec c1; control_rec c2