Renommage AppL en App

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

9 files changed, 19 insertions, 19 deletions

diff --git a/pretyping/class.ml b/pretyping/class.ml
index f9c36315b6..b83eb3608f 100644
--- a/pretyping/class.ml
+++ b/pretyping/class.ml
@@ -110,7 +110,7 @@ let check_class id v cl p =
 
 (* decomposition de constr vers coe_typ *)
 
-(* t provient de global_reference donc pas de Cast, pas de AppL *)
+(* t provient de global_reference donc pas de Cast, pas de App *)
 let coe_of_reference t = 
   match kind_of_term t with
     | IsConst (sp,l) -> (Array.to_list l),NAM_Constant sp
@@ -126,7 +126,7 @@ let constructor_at_head1 t =
       | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0
       | IsVar id -> t',[],[],CL_Var id,0
       | IsCast (c,_) -> aux c
-      | IsAppL(f,args) -> 
+      | IsApp(f,args) -> 
 	  let t',_,l,c,_ = aux f in t',Array.to_list args,l,c,Array.length args
       | IsProd (_,_,_) -> t',[],[],CL_FUN,0
       | IsLetIn (_,_,_,c) -> aux c
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index d8475e50e3..36b5ed4d53 100755
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -196,7 +196,7 @@ let constructor_at_head t =
     | IsLetIn (_,_,_,c) -> aux c
     | IsSort _ -> CL_SORT,0
     | IsCast (c,_) -> aux (collapse_appl c)
-    | IsAppL (f,args) -> let c,_ = aux f in c, Array.length args
+    | IsApp (f,args) -> let c,_ = aux f in c, Array.length args
     |  _ -> raise Not_found
   in 
   aux (collapse_appl t)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 2892cddb43..839cfac4f1 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -147,7 +147,7 @@ let rec inh_conv_coerce_to_fail env isevars c1 hj =
 		   {uj_val = mkRel 1; 
 		    uj_type = typed_app (fun _ -> u1) assu1 } in
                let h2 = inh_conv_coerce_to_fail env isevars u2  
-			 { uj_val = mkAppL (lift 1 v, [|h1.uj_val|]);
+			 { uj_val = mkApp (lift 1 v, [|h1.uj_val|]);
                            uj_type = get_assumption_of env1 !isevars
 				       (subst1 h1.uj_val t2) }
 	       in
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index dd3022764a..a02cf96a66 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -282,7 +282,7 @@ let rec detype avoid env t =
     | IsProd (na,ty,c) -> detype_binder BProd avoid env na ty c
     | IsLambda (na,ty,c) -> detype_binder BLambda avoid env na ty c
     | IsLetIn (na,b,_,c) -> detype_binder BLetIn avoid env na b c
-    | IsAppL (f,args) ->
+    | IsApp (f,args) ->
 	RApp (dummy_loc,detype avoid env f,array_map_to_list (detype avoid env) args)
     | IsConst (sp,cl) ->
 	RRef(dummy_loc,RConst(sp,Array.map (detype avoid env) cl))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index d3b9c04f6f..b877624ada 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -300,8 +300,8 @@ and evar_eqappr_x env isevars pbty (term1,l1 as appr1) (term2,l2 as appr2) =
     | (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _), _ -> false
     | _, (IsMutInd _ | IsMutConstruct _ | IsSort _ | IsProd _) -> false
 
-    | (IsAppL _ | IsMutCase _ | IsFix _ | IsCoFix _), 
-      (IsAppL _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false
+    | (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _), 
+      (IsApp _ | IsMutCase _ | IsFix _ | IsCoFix _) -> false
 
 
 
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 6407284be6..b7061962bf 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -337,14 +337,14 @@ let has_undefined_isevars isevars c =
 let head_is_exist isevars = 
   let rec hrec k = match kind_of_term k with
     | IsEvar _     -> ise_undefined isevars k
-    | IsAppL (f,_) -> hrec f
+    | IsApp (f,_) -> hrec f
     | IsCast (c,_) -> hrec c
     | _ -> false
   in 
   hrec 
 
 let rec is_eliminator c = match kind_of_term c with
-  | IsAppL _    -> true
+  | IsApp _    -> true
   | IsMutCase _ -> true
   | IsCast (c,_) -> is_eliminator c
   | _ -> false
@@ -356,7 +356,7 @@ let head_evar =
   let rec hrec c = match kind_of_term c with
     | IsEvar (ev,_)       -> ev
     | IsMutCase (_,_,c,_) -> hrec c
-    | IsAppL (c,_)        -> hrec c
+    | IsApp (c,_)        -> hrec c
     | IsCast (c,_)        -> hrec c
     | _                   -> failwith "headconstant"
   in 
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 0bae65053c..1e7da45794 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -70,7 +70,7 @@ let rec type_of env cstr=
          subst1 b (type_of (push_rel_def (name,b,var) env) c2)
     | IsFix ((vn,i),(lar,lfi,vdef)) -> lar.(i)
     | IsCoFix (i,(lar,lfi,vdef)) -> lar.(i)
-    | IsAppL(f,args)->
+    | IsApp(f,args)->
       strip_outer_cast (subst_type env sigma (type_of env f) 
 			  (Array.to_list args))
     | IsCast (c,t) -> t
@@ -87,7 +87,7 @@ and sort_of env t =
         (match (sort_of (push_rel_decl (name,var) env) c2) with
 	  | Prop _ as s -> s
 	  | Type u2 -> Type Univ.dummy_univ)
-    | IsAppL(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
+    | IsApp(f,args) -> sort_of_atomic_type env sigma (type_of env f) args
     | IsLambda _ | IsFix _ | IsMutConstruct _ ->
         anomaly "sort_of: Not a type (1)"
     | _ -> outsort env sigma (type_of env t)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 2c324609aa..80948207a7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -250,7 +250,7 @@ and construct_const env sigma =
 		| None ->
 		    raise Redelimination))
       | IsCast (c,_) -> hnfstack (c, stack)
-      | IsAppL (f,cl) -> hnfstack (f, append_stack cl stack)
+      | IsApp (f,cl) -> hnfstack (f, append_stack cl stack)
       | IsLambda (_,_,c) ->
           (match decomp_stack stack with 
              | None -> assert false
@@ -276,7 +276,7 @@ and construct_const env sigma =
 let internal_red_product env sigma c = 
   let rec redrec x =
     match kind_of_term x with
-      | IsAppL (f,l) -> appvect (redrec f, l)
+      | IsApp (f,l) -> appvect (redrec f, l)
       | IsConst cst -> constant_value env cst
       | IsEvar ev -> existential_value sigma ev
       | IsCast (c,_) -> redrec c
@@ -302,7 +302,7 @@ let hnf_constr env sigma c =
              | None      -> app_stack s
              | Some (a,rest) -> stacklam redrec [a] c rest)
       | IsLetIn (n,b,_,c) -> stacklam redrec [b] c largs
-      | IsAppL (f,cl)   -> redrec (f, append_stack cl largs)
+      | IsApp (f,cl)   -> redrec (f, append_stack cl largs)
       | IsConst cst ->
           (try
              let (c',lrest) = red_elim_const env sigma x largs in 
@@ -341,7 +341,7 @@ let whd_nf env sigma c =
              | None -> (c,empty_stack)
              | Some (a1,rest) -> stacklam nf_app [a1] c2 rest)
       | IsLetIn (n,b,_,c) -> stacklam nf_app [b] c stack
-      | IsAppL (f,cl) -> nf_app (f, append_stack cl stack)
+      | IsApp (f,cl) -> nf_app (f, append_stack cl stack)
       | IsCast (c,_) -> nf_app (c, stack)
       | IsConst _ ->
           (try
@@ -381,7 +381,7 @@ let rec substlin env name n ol c =
 	  ((n+1),ol,c)
 
     (* INEFFICIENT: OPTIMIZE *)
-    | IsAppL (c1,cl) ->
+    | IsApp (c1,cl) ->
         Array.fold_left 
 	  (fun (n1,ol1,c1') c2 ->
 	     (match ol1 with 
@@ -547,7 +547,7 @@ let one_step_reduce env sigma c =
           (match decomp_stack largs with
              | None      -> error "Not reducible 1"
              | Some (a,rest) -> (subst1 a c, rest))
-      | IsAppL (f,cl) -> redrec (f, append_stack cl largs)
+      | IsApp (f,cl) -> redrec (f, append_stack cl largs)
       | IsConst cst ->
           (try
              red_elim_const env sigma x largs
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index b946911e06..8b9319a29c 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -77,7 +77,7 @@ let rec execute mf env sigma cstr =
     | IsSort (Type u) ->
 	let (j,_) = judge_of_type u in j
 	  
-    | IsAppL (f,args) ->
+    | IsApp (f,args) ->
 	let j = execute mf env sigma f in
         let jl = execute_list mf env sigma (Array.to_list args) in
 	let (j,_) = apply_rel_list env sigma mf.nocheck jl j in