Uniformisation de destApplication en destApp

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

5 files changed, 9 insertions, 9 deletions

diff --git a/contrib/cc/cctac.ml4 b/contrib/cc/cctac.ml4
index 98ea8e495..799867675 100644
--- a/contrib/cc/cctac.ml4
+++ b/contrib/cc/cctac.ml4
@@ -126,7 +126,7 @@ let make_prb gl=
 let build_projection intype outtype (cstr:constructor) special default gls=
   let env=pf_env gls in 
   let (h,argv) = 
-    try destApplication intype with 
+    try destApp intype with 
 	Invalid_argument _ -> (intype,[||])  in
   let ind=destInd h in 
   let types=Inductiveops.arities_of_constructors env ind in
diff --git a/contrib/funind/tacinv.ml4 b/contrib/funind/tacinv.ml4
index cc2cd90fc..c2a421e7e 100644
--- a/contrib/funind/tacinv.ml4
+++ b/contrib/funind/tacinv.ml4
@@ -650,7 +650,7 @@ let rec applistc_iota cstr lcstr env sigma =
   | [] -> cstr,[]
   | arg::lcstr' -> 
      let arghd = 
-      if isApp arg then let x,_ = destApplication arg in x else arg in
+      if isApp arg then let x,_ = destApp arg in x else arg in
      if isConstruct arghd (* of the form [(C ...)]*)
      then 
         applistc_iota (Tacred.nf env sigma (nf_beta (applistc cstr [arg])))
diff --git a/contrib/funind/tacinvutils.ml b/contrib/funind/tacinvutils.ml
index 1da7fcb4b..6f8223575 100644
--- a/contrib/funind/tacinvutils.ml
+++ b/contrib/funind/tacinvutils.ml
@@ -126,7 +126,7 @@ let apply_leqtrpl_t t leq =
 
 
 let apply_refl_term eq t =
-  let _,arr = destApplication eq in
+  let _,arr = destApp eq in
   let reli= (Array.get arr 1) in
   let by_t= (Array.get arr 2) in
   substitterm 0 reli by_t t
@@ -144,7 +144,7 @@ let apply_eq_leqtrpl leq eq =
 let constr_head_match u t=
   if isApp u 
   then 
-	 let uhd,args= destApplication u in
+	 let uhd,args= destApp u in
     uhd=t
   else false
 
@@ -187,7 +187,7 @@ let rec buildrefl_from_eqs eqs =
   match eqs with 
     | []  ->  []
     | cstr::eqs' -> 
-        let eq,args = destApplication cstr in
+        let eq,args = destApp cstr in
         (mkRefl (Array.get args 0) (Array.get args 2))
 	:: (buildrefl_from_eqs eqs')
 
@@ -218,7 +218,7 @@ let hdMatchSub_cpl u (d,f) =
 
 (* destApplication raises an exception if [t] is not an application *)      
 let exchange_hd_prod subst_hd t =
-    let (hd,args)= destApplication t in mkApp (subst_hd,args)
+    let (hd,args)= destApp t in mkApp (subst_hd,args)
 
 (* substitute t by by_t in head of products inside in_u, reduces each
 	product found  *)
@@ -237,7 +237,7 @@ let rec substit_red prof t by_t in_u =
 (* [exchange_reli_arrayi t=(reli x y ...) tarr (d,f)] exchange each
 	reli by tarr.(f-i). *) 
 let exchange_reli_arrayi tarr (d,f) t =
-  let hd,args= destApplication t in 
+  let hd,args= destApp t in 
   let i = destRel hd in
   whd_beta (mkApp (tarr.(f-i) ,args))
 
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index a2c2cc770..5ef84adc7 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -299,7 +299,7 @@ let constructor_instantiate mind mib params ctyp =
     let sp = List.rev (Array.to_list params) in substl sp ctyp2
   
 let destApplication t =
-  try destApplication t 
+  try destApp t 
   with _ -> t,[||]
 
 let construct_of_constr_const env tag typ =
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index ce09bf8aa..ee854e951 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -608,7 +608,7 @@ let contextually byhead (locs,c) f env sigma t =
 	f env sigma t
       else if byhead then
 	(* find other occurrences of c in t; TODO: ensure left-to-right *)
-        let (f,l) = destApplication t in
+        let (f,l) = destApp t in
 	mkApp (f, array_map_left (traverse envc) l)
       else
 	t