diff options
-rw-r--r-- | contrib/cc/cctac.ml4 | 2 | ||||
-rw-r--r-- | contrib/funind/tacinv.ml4 | 2 | ||||
-rw-r--r-- | contrib/funind/tacinvutils.ml | 10 | ||||
-rw-r--r-- | kernel/vconv.ml | 2 | ||||
-rw-r--r-- | pretyping/tacred.ml | 2 |
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 |