Renommage AppL en App

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

2 files changed, 26 insertions, 26 deletions

diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml
index f16b6049ed..a3dd19dd68 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 7c514bd2a9..d2064380b2 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