Renommage AppL en App

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

6 files changed, 20 insertions, 20 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index f260604cf9..07219dd359 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -617,7 +617,7 @@ let discr id gls =
 	 in
 	 tclCOMPLETE((tclTHENS (cut_intro absurd_term)
 			([onLastHyp (compose gen_absurdity out_some);
-			  refine (mkAppL (pf, [| mkVar id |]))]))) gls)
+			  refine (mkApp (pf, [| mkVar id |]))]))) gls)
 
 
 let not_found_message id =
@@ -856,7 +856,7 @@ let try_delta_expand env sigma t =
   let rec hd_rec c  =
     match kind_of_term c with
       | IsMutConstruct _ -> whdt
-      | IsAppL (f,_)  -> hd_rec f
+      | IsApp (f,_)  -> hd_rec f
       | IsCast (c,_) -> hd_rec c
       | _  -> t
   in 
@@ -959,7 +959,7 @@ let decompEqThen ntac id gls =
 	 tclCOMPLETE
 	   ((tclTHENS (cut_intro absurd_term)
 	       ([onLastHyp (compose gen_absurdity out_some);
-		 refine (mkAppL (pf, [| mkVar id |]))]))) gls
+		 refine (mkApp (pf, [| mkVar id |]))]))) gls
      | Inr posns ->
 	 (let e = pf_get_new_id (id_of_string "e") gls in
 	  let e_env =
@@ -1179,7 +1179,7 @@ let whd_const_state namelist env sigma =
           else 
 	    error "whd_const_stack"
       | IsCast (c,_) -> whrec (c, l)
-      | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+      | IsApp (f,cl) -> whrec (f, append_stack cl l)
       | _ -> s
   in 
   whrec
@@ -1310,7 +1310,7 @@ let rec eq_mod_rel l_meta t0 t1 =
 (* Verifies if the constr has an head constant *)
 
 let is_hd_const c = match kind_of_term c with
-  | IsAppL (f,args) ->
+  | IsApp (f,args) ->
       (match kind_of_term f with
          | IsConst (c,_) -> Some (c, args)
          |_ -> None)
@@ -1335,7 +1335,7 @@ let nb_occ_term t u =
 *)
 let sub_term_with_unif cref ceq =
   let rec find_match l_meta nb_occ hdsp t_args u = match splay_constr u with
-    | OpAppL, cl -> begin
+    | OpApp, cl -> begin
 	let f, args = destApplication u in
 	match kind_of_term f with
           | IsConst (sp,_) when sp = hdsp -> begin
diff --git a/tactics/hipattern.ml b/tactics/hipattern.ml
index d9d81238b8..1f78dcb85a 100644
--- a/tactics/hipattern.ml
+++ b/tactics/hipattern.ml
@@ -96,7 +96,7 @@ let op2bool = function Some _ -> true | None -> false
 
 let match_with_non_recursive_type t = 
   match kind_of_term t with 
-    | IsAppL _ -> 
+    | IsApp _ -> 
         let (hdapp,args) = decomp_app t in
         (match kind_of_term hdapp with
            | IsMutInd ind -> 
diff --git a/tactics/refine.ml b/tactics/refine.ml
index 53cced1616..f3bd862a3f 100644
--- a/tactics/refine.ml
+++ b/tactics/refine.ml
@@ -95,7 +95,7 @@ let replace_by_meta env = function
 	    mkNamedProd id c1 (snd (destCast c2))
 	| IsLambda (Anonymous,c1,c2) when isCast c2 ->
 	    mkArrow c1 (snd (destCast c2))
-	| (IsAppL _ | IsMutCase _) ->
+	| (IsApp _ | IsMutCase _) ->
 	    (** let j = ise_resolve true empty_evd mm (gLOB sign) c in **)
 	    Retyping.get_type_of_with_meta env Evd.empty mm c
 	| IsFix ((_,j),(v,_,_)) ->
@@ -153,7 +153,7 @@ let rec compute_metamap env c = match kind_of_term c with
       compute_metamap env (subst1 c1 c2)
 
   (* 4. Application *)
-  | IsAppL (f,v) ->
+  | IsApp (f,v) ->
       let a = Array.map (compute_metamap env) (Array.append [|f|] v) in
       begin
 	try
@@ -260,7 +260,7 @@ let rec tcc_aux (TH (c,mm,sgp) as th) gl =
 	  gl
 
     (* sinon on fait refine du terme puis appels rec. sur les sous-buts.
-     * c'est le cas pour AppL et MutCase. *)
+     * c'est le cas pour App et MutCase. *)
     | _ ->
 	tclTHENS
 	  (refine c)
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index feb48e4ef9..1ed2e536b4 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -290,7 +290,7 @@ let sort_of_goal gl =
 (* c should be of type A1->.. An->B with B an inductive definition *)
 
 let last_arg c = match kind_of_term c with
-  | IsAppL (f,cl) -> array_last cl
+  | IsApp (f,cl) -> array_last cl
   | _ -> anomaly "last_arg"
 
 let general_elim_then_using 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3f864682e4..0c84518701 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -59,7 +59,7 @@ let rec head_constr_bound t l =
   let t = strip_outer_cast(collapse_appl t) in
   match kind_of_term t with
     | IsProd (_,_,c2)  -> head_constr_bound c2 l 
-    | IsAppL (f,args)  -> 
+    | IsApp (f,args)  -> 
 	head_constr_bound f (Array.fold_right (fun a l -> a::l) args l)
     | IsConst _        -> t::l
     | IsMutInd _       -> t::l
@@ -930,7 +930,7 @@ let dyn_split  = function
 *)
 
 let last_arg c = match kind_of_term c with
-  | IsAppL (f,cl) ->  array_last cl
+  | IsApp (f,cl) ->  array_last cl
   | _ -> anomaly "last_arg"
 	
 let elimination_clause_scheme kONT wc elimclause indclause gl = 
@@ -1572,8 +1572,8 @@ let symmetry gl =
 	    (apply (pf_parse_const gl ("sym_"^hdcncls)) gl)
           with  _ ->
             let symc = match args with 
-              | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; c2; c1 |])
-              | [c1;c2]     -> mkAppL (hdcncl, [| c2; c1 |])
+              | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c2; c1 |])
+              | [c1;c2]     -> mkApp (hdcncl, [| c2; c1 |])
 	      | _ -> assert false 
 	    in 
 	    (tclTHENS (cut symc)
@@ -1611,13 +1611,13 @@ let transitivity t gl =
 	    apply_list [(pf_parse_const gl ("trans_"^hdcncls));t] gl 
           with  _ -> 
             let eq1 = match args with 
-              | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; c1; t |])
-	      | [c1;c2]     -> mkAppL (hdcncl, [| c1; t|])
+              | [typ;c1;c2] -> mkApp (hdcncl, [| typ; c1; t |])
+	      | [c1;c2]     -> mkApp (hdcncl, [| c1; t|])
 	      | _ -> assert false 
 	    in
             let eq2 = match args with 
-              | [typ;c1;c2] -> mkAppL (hdcncl, [| typ; t; c2 |])
-	      | [c1;c2]     -> mkAppL (hdcncl, [| t; c2 |])
+              | [typ;c1;c2] -> mkApp (hdcncl, [| typ; t; c2 |])
+	      | [c1;c2]     -> mkApp (hdcncl, [| t; c2 |])
 	      |  _ -> assert false 
 	    in
             (tclTHENS (cut eq2)
diff --git a/tactics/termdn.ml b/tactics/termdn.ml
index 1837b7945e..3a1df02349 100644
--- a/tactics/termdn.ml
+++ b/tactics/termdn.ml
@@ -18,7 +18,7 @@ type 'a t = (constr_label,constr_pattern,'a) Dn.t
 
 let decomp = 
   let rec decrec acc c = match kind_of_term c with
-    | IsAppL (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
+    | IsApp (f,l) -> decrec (Array.fold_right (fun a l -> a::l) l acc) f
     | IsCast (c1,_) -> decrec acc c1
     | _ -> (c,acc)
   in