aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/closure.ml12
-rw-r--r--kernel/environ.ml2
-rw-r--r--kernel/reduction.ml34
-rw-r--r--kernel/safe_typing.ml2
-rw-r--r--kernel/term.ml102
-rw-r--r--kernel/term.mli16
-rw-r--r--kernel/typeops.ml4
-rw-r--r--library/indrec.ml8
-rw-r--r--parsing/pattern.ml10
-rw-r--r--parsing/pretty.ml4
-rw-r--r--parsing/termast.ml2
-rw-r--r--pretyping/class.ml4
-rwxr-xr-xpretyping/classops.ml2
-rw-r--r--pretyping/coercion.ml2
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/evarutil.ml6
-rw-r--r--pretyping/retyping.ml4
-rw-r--r--pretyping/tacred.ml12
-rw-r--r--pretyping/typing.ml2
-rw-r--r--proofs/clenv.ml16
-rw-r--r--proofs/logic.ml8
-rw-r--r--tactics/equality.ml12
-rw-r--r--tactics/hipattern.ml2
-rw-r--r--tactics/refine.ml6
-rw-r--r--tactics/tacticals.ml2
-rw-r--r--tactics/tactics.ml16
-rw-r--r--tactics/termdn.ml2
28 files changed, 146 insertions, 152 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml
index 0bb893c6f..f18d7e077 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -388,7 +388,7 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
subst_bodies_from_i 0 env, bds.(i)
-(* type of terms with a hole. This hole can appear only under AppL or Case.
+(* type of terms with a hole. This hole can appear only under App or Case.
* TOP means the term is considered without context
* APP(l,stk) means the term is applied to l, and then we have the context st
* this corresponds to the application stack of the KAM.
@@ -499,7 +499,7 @@ let rec norm_head info env t stack =
(* no reduction under binders *)
match kind_of_term t with
(* stack grows (remove casts) *)
- | IsAppL (head,args) -> (* Applied terms are normalized immediately;
+ | IsApp (head,args) -> (* Applied terms are normalized immediately;
they could be computed when getting out of the stack *)
let nargs = Array.map (cbv_stack_term info TOP env) args in
norm_head info env head (stack_app (Array.to_list nargs) stack)
@@ -810,7 +810,7 @@ let rec traverse_term env t =
| IsCast (a,b) ->
{ norm = false;
term = FCast (traverse_term env a, traverse_term env b)}
- | IsAppL (f,v) ->
+ | IsApp (f,v) ->
{ norm = false;
term = FApp (traverse_term env f, Array.map (traverse_term env) v) }
| IsMutInd (sp,v) ->
@@ -889,7 +889,7 @@ let rec lift_term_of_freeze lfts v =
mkCoFix (op, (Array.map (lift_term_of_freeze lfts) tys, lna,
Array.map (lift_term_of_freeze lfts') bds))
| FApp (f,ve) ->
- mkAppL (lift_term_of_freeze lfts f,
+ mkApp (lift_term_of_freeze lfts f,
Array.map (lift_term_of_freeze lfts) ve)
| FLambda (n,t,c,_,_) ->
mkLambda (n, lift_term_of_freeze lfts t,
@@ -945,7 +945,7 @@ let rec fstrong unfreeze_fun lfts v =
mkCoFix (op, (Array.map (fstrong unfreeze_fun lfts) tys, lna,
Array.map (fstrong unfreeze_fun lfts') bds))
| FApp (f,ve) ->
- mkAppL (fstrong unfreeze_fun lfts f,
+ mkApp (fstrong unfreeze_fun lfts f,
Array.map (fstrong unfreeze_fun lfts) ve)
| FLambda (n,t,c,_,_) ->
mkLambda (n, fstrong unfreeze_fun lfts t,
@@ -1172,7 +1172,7 @@ and whnf_term info env t =
| IsSort _ | IsXtra _ | IsMeta _ -> {norm = true; term = FAtom t }
| IsCast (c,_) -> whnf_term info env c (* remove outer casts *)
- | IsAppL (f,ve) ->
+ | IsApp (f,ve) ->
whnf_frterm info
{ norm = false; term = FApp (freeze env f, freeze_vect env ve)}
| IsConst (op,ve) ->
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 456e89bad..100db950f 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -216,7 +216,7 @@ let hdchar env c =
| IsLambda (_,_,c) -> hdrec (k+1) c
| IsLetIn (_,_,_,c) -> hdrec (k+1) c
| IsCast (c,_) -> hdrec k c
- | IsAppL (f,l) -> hdrec k f
+ | IsApp (f,l) -> hdrec k f
| IsConst (sp,_) ->
let c = lowercase_first_char (basename sp) in
if c = "?" then "y" else c
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 84b5b7a07..827956fd5 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -98,7 +98,7 @@ let append_stack v s = v@s
let rec whd_state (x, stack as s) =
match kind_of_term x with
- | IsAppL (f,cl) -> whd_state (f, append_stack cl stack)
+ | IsApp (f,cl) -> whd_state (f, append_stack cl stack)
| IsCast (c,_) -> whd_state (c, stack)
| _ -> s
@@ -278,13 +278,13 @@ let whd_state_gen flags env sigma =
| None -> s)
| IsLetIn (_,b,_,c) when red_letin flags -> stacklam whrec [b] c stack
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
| Some (a,m) when red_beta flags -> stacklam whrec [a] c m
| None when red_eta flags ->
(match kind_of_term (app_stack (whrec (c, empty_stack))) with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
let x', l' = whrec (array_last cl, empty_stack) in
@@ -321,13 +321,13 @@ let local_whd_state_gen flags =
match kind_of_term x with
| IsLetIn (_,b,_,c) when red_delta flags -> stacklam whrec [b] c stack
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
| Some (a,m) when red_beta flags -> stacklam whrec [a] c m
| None when red_eta flags ->
(match kind_of_term (app_stack (whrec (c, empty_stack))) with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
let x', l' = whrec (array_last cl, empty_stack) in
@@ -370,7 +370,7 @@ let whd_beta_state =
| Some (a1,rest) -> stacklam whrec [a1] c2 rest)
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| x -> s
in
whrec
@@ -392,7 +392,7 @@ let whd_delta_state env sigma =
whrec (existential_value sigma (ev,args), l)
| IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
| IsCast (c,_) -> whrec (c, l)
- | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+ | IsApp (f,cl) -> whrec (f, append_stack cl l)
| x -> s
in
whrec
@@ -420,7 +420,7 @@ let whd_betadelta_state env sigma =
s
| IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
| IsCast (c,_) -> whrec (c, l)
- | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+ | IsApp (f,cl) -> whrec (f, append_stack cl l)
| IsLambda (_,_,c) ->
(match decomp_stack l with
| None -> s
@@ -447,7 +447,7 @@ let whd_betaevar_stack env sigma =
else
s
| IsCast (c,_) -> whrec (c, l)
- | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+ | IsApp (f,cl) -> whrec (f, append_stack cl l)
| IsLambda (_,_,c) ->
(match decomp_stack l with
| None -> s
@@ -473,12 +473,12 @@ let whd_betadeltaeta_state env sigma =
whrec (existential_value sigma (ev,args), l)
| IsLetIn (_,b,_,c) -> stacklam whrec [b] c l
| IsCast (c,_) -> whrec (c, l)
- | IsAppL (f,cl) -> whrec (f, append_stack cl l)
+ | IsApp (f,cl) -> whrec (f, append_stack cl l)
| IsLambda (_,_,c) ->
(match decomp_stack l with
| None ->
(match kind_of_term (app_stack (whrec (c, empty_stack))) with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
let x',l' = whrec (array_last cl, empty_stack) in
@@ -514,7 +514,7 @@ let whd_betaiota_state =
let rec whrec (x,stack as s) =
match kind_of_term x with
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
| None -> s
@@ -553,7 +553,7 @@ let whd_betaiotaevar_state env sigma =
else
s
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
| None -> s
@@ -591,7 +591,7 @@ let whd_betadeltaiota_state env sigma =
whrec (existential_value sigma (ev,args), stack)
| IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
| None -> s
@@ -629,12 +629,12 @@ let whd_betadeltaiotaeta_state env sigma =
whrec (existential_value sigma (ev,args), stack)
| IsLetIn (_,b,_,c) -> stacklam whrec [b] c stack
| IsCast (c,_) -> whrec (c, stack)
- | IsAppL (f,cl) -> whrec (f, append_stack cl stack)
+ | IsApp (f,cl) -> whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
| None ->
(match kind_of_term (app_stack (whrec (c, empty_stack))) with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let napp = Array.length cl in
if napp > 0 then
let x', l' = whrec (array_last cl, empty_stack) in
@@ -1062,7 +1062,7 @@ let hnf env sigma c = apprec env sigma (c, empty_stack)
let whd_programs_stack env sigma =
let rec whrec (x, stack as s) =
match kind_of_term x with
- | IsAppL (f,([|c|] as cl)) ->
+ | IsApp (f,([|c|] as cl)) ->
if occur_meta c then s else whrec (f, append_stack cl stack)
| IsLambda (_,_,c) ->
(match decomp_stack stack with
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 5c1493e2a..f1b97bcd2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -92,7 +92,7 @@ let rec execute mf env cstr =
| IsSort (Type u) ->
judge_of_type u
- | IsAppL (f,args) ->
+ | IsApp (f,args) ->
let (j,cst1) = execute mf env f in
let (jl,cst2) = execute_array mf env args in
let (j,cst3) =
diff --git a/kernel/term.ml b/kernel/term.ml
index 38e3f5bfe..9829c1154 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -67,7 +67,7 @@ type kind_of_term =
| IsProd of name * constr * constr
| IsLambda of name * constr * constr
| IsLetIn of name * constr * constr * constr
- | IsAppL of constr * constr array
+ | IsApp of constr * constr array
| IsEvar of existential
| IsConst of constant
| IsMutInd of inductive
@@ -85,7 +85,7 @@ val mkCast : constr * constr -> constr
val mkProd : name * constr * constr -> constr
val mkLambda : name * constr * constr -> constr
val mkLetIn : name * constr * constr * constr -> constr
-val mkAppL : constr * constr array -> constr
+val mkApp : constr * constr array -> constr
val mkEvar : existential -> constr
val mkConst : constant -> constr
val mkMutInd : inductive -> constr
@@ -129,7 +129,7 @@ and kind_of_term =
| IsProd of name * constr * constr
| IsLambda of name * constr * constr
| IsLetIn of name * constr * constr * constr
- | IsAppL of constr * constr array
+ | IsApp of constr * constr array
| IsEvar of existential
| IsConst of constant
| IsMutInd of inductive
@@ -154,7 +154,7 @@ let comp_term t1 t2 =
| IsLambda (n1,t1,c1), IsLambda (n2,t2,c2) -> n1 == n2 & t1 == t2 & c1 == c2
| IsLetIn (n1,b1,t1,c1), IsLetIn (n2,b2,t2,c2) ->
n1 == n2 & b1 == b2 & t1 == t2 & c1 == c2
- | IsAppL (c1,l1), IsAppL (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
+ | IsApp (c1,l1), IsApp (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
| IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 (==) l1 l2
| IsConst (c1,l1), IsConst (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
| IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 == c2 & array_for_all2 (==) l1 l2
@@ -180,7 +180,7 @@ let hash_term (sh_rec,(sh_sort,sh_sp,sh_na,sh_id,sh_str)) t =
| IsProd (na,t,c) -> IsProd (sh_na na, sh_rec t, sh_rec c)
| IsLambda (na,t,c) -> IsLambda (sh_na na, sh_rec t, sh_rec c)
| IsLetIn (na,b,t,c) -> IsLetIn (sh_na na, sh_rec b, sh_rec t, sh_rec c)
- | IsAppL (c,l) -> IsAppL (sh_rec c, Array.map sh_rec l)
+ | IsApp (c,l) -> IsApp (sh_rec c, Array.map sh_rec l)
| IsEvar (e,l) -> IsEvar (e, Array.map sh_rec l)
| IsConst (c,l) -> IsConst (sh_sp c, Array.map sh_rec l)
| IsMutInd ((sp,i),l) -> IsMutInd ((sh_sp sp,i), Array.map sh_rec l)
@@ -242,11 +242,11 @@ let mkLetIn (x,c1,t,c2) = IsLetIn (x,c1,t,c2)
(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
(* We ensure applicative terms have at most one arguments and the
function is not itself an applicative term *)
-let mkAppL (f, a) =
+let mkApp (f, a) =
if a=[||] then f else
match f with
- | IsAppL (g, cl) -> IsAppL (g, Array.append cl a)
- | _ -> IsAppL (f, a)
+ | IsApp (g, cl) -> IsApp (g, Array.append cl a)
+ | _ -> IsApp (f, a)
(* Constructs a constant *)
@@ -297,7 +297,7 @@ open Internal
END of expected re-export of Internal module *)
-(* User view of [constr]. For [IsAppL], it is ensured there is at
+(* User view of [constr]. For [IsApp], it is ensured there is at
least one argument and the function is not itself an applicative
term *)
@@ -420,10 +420,10 @@ let destLetIn c = match kind_of_term c with
(* Destructs an application *)
let destApplication c = match kind_of_term c with
- | IsAppL (f,a) -> (f, a)
+ | IsApp (f,a) -> (f, a)
| _ -> invalid_arg "destApplication"
-let isAppL c = match kind_of_term c with IsAppL _ -> true | _ -> false
+let isApp c = match kind_of_term c with IsApp _ -> true | _ -> false
(* Destructs a constant *)
let destConst c = match kind_of_term c with
@@ -505,7 +505,7 @@ let fold_constr f acc c = match kind_of_term c with
| IsProd (_,t,c) -> f (f acc t) c
| IsLambda (_,t,c) -> f (f acc t) c
| IsLetIn (_,b,t,c) -> f (f (f acc b) t) c
- | IsAppL (c,l) -> Array.fold_left f (f acc c) l
+ | IsApp (c,l) -> Array.fold_left f (f acc c) l
| IsEvar (_,l) -> Array.fold_left f acc l
| IsConst (_,l) -> Array.fold_left f acc l
| IsMutInd (_,l) -> Array.fold_left f acc l
@@ -529,7 +529,7 @@ let fold_constr_with_binders g f n acc c = match kind_of_term c with
| IsProd (_,t,c) -> f (g n) (f n acc t) c
| IsLambda (_,t,c) -> f (g n) (f n acc t) c
| IsLetIn (_,b,t,c) -> f (g n) (f n (f n acc b) t) c
- | IsAppL (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | IsApp (c,l) -> Array.fold_left (f n) (f n acc c) l
| IsEvar (_,l) -> Array.fold_left (f n) acc l
| IsConst (_,l) -> Array.fold_left (f n) acc l
| IsMutInd (_,l) -> Array.fold_left (f n) acc l
@@ -552,7 +552,7 @@ let iter_constr f c = match kind_of_term c with
| IsProd (_,t,c) -> f t; f c
| IsLambda (_,t,c) -> f t; f c
| IsLetIn (_,b,t,c) -> f b; f t; f c
- | IsAppL (c,l) -> f c; Array.iter f l
+ | IsApp (c,l) -> f c; Array.iter f l
| IsEvar (_,l) -> Array.iter f l
| IsConst (_,l) -> Array.iter f l
| IsMutInd (_,l) -> Array.iter f l
@@ -573,7 +573,7 @@ let iter_constr_with_binders g f n c = match kind_of_term c with
| IsProd (_,t,c) -> f n t; f (g n) c
| IsLambda (_,t,c) -> f n t; f (g n) c
| IsLetIn (_,b,t,c) -> f n b; f n t; f (g n) c
- | IsAppL (c,l) -> f n c; Array.iter (f n) l
+ | IsApp (c,l) -> f n c; Array.iter (f n) l
| IsEvar (_,l) -> Array.iter (f n) l
| IsConst (_,l) -> Array.iter (f n) l
| IsMutInd (_,l) -> Array.iter (f n) l
@@ -594,7 +594,7 @@ let map_constr f c = match kind_of_term c with
| IsProd (na,t,c) -> mkProd (na, f t, f c)
| IsLambda (na,t,c) -> mkLambda (na, f t, f c)
| IsLetIn (na,b,t,c) -> mkLetIn (na, f b, f t, f c)
- | IsAppL (c,l) -> mkAppL (f c, Array.map f l)
+ | IsApp (c,l) -> mkApp (f c, Array.map f l)
| IsEvar (e,l) -> mkEvar (e, Array.map f l)
| IsConst (c,l) -> mkConst (c, Array.map f l)
| IsMutInd (c,l) -> mkMutInd (c, Array.map f l)
@@ -615,7 +615,7 @@ let map_constr_with_binders g f l c = match kind_of_term c with
| IsProd (na,t,c) -> mkProd (na, f l t, f (g l) c)
| IsLambda (na,t,c) -> mkLambda (na, f l t, f (g l) c)
| IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g l) c)
- | IsAppL (c,al) -> mkAppL (f l c, Array.map (f l) al)
+ | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
| IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
| IsConst (c,al) -> mkConst (c, Array.map (f l) al)
| IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
@@ -640,7 +640,7 @@ let map_constr_with_named_binders g f l c = match kind_of_term c with
| IsProd (na,t,c) -> mkProd (na, f l t, f (g na l) c)
| IsLambda (na,t,c) -> mkLambda (na, f l t, f (g na l) c)
| IsLetIn (na,b,t,c) -> mkLetIn (na, f l b, f l t, f (g na l) c)
- | IsAppL (c,al) -> mkAppL (f l c, Array.map (f l) al)
+ | IsApp (c,al) -> mkApp (f l c, Array.map (f l) al)
| IsEvar (e,al) -> mkEvar (e, Array.map (f l) al)
| IsConst (c,al) -> mkConst (c, Array.map (f l) al)
| IsMutInd (c,al) -> mkMutInd (c, Array.map (f l) al)
@@ -693,8 +693,8 @@ let map_constr_with_binders_left_to_right g f l c = match kind_of_term c with
| IsLambda (na,t,c) -> let t' = f l t in mkLambda (na, t', f (g l) c)
| IsLetIn (na,b,t,c) ->
let b' = f l b in let t' = f l t in mkLetIn (na, b', t', f (g l) c)
- | IsAppL (c,al) ->
- let c' = f l c in mkAppL (c', array_map_left (f l) al)
+ | IsApp (c,al) ->
+ let c' = f l c in mkApp (c', array_map_left (f l) al)
| IsEvar (e,al) -> mkEvar (e, array_map_left (f l) al)
| IsConst (c,al) -> mkConst (c, array_map_left (f l) al)
| IsMutInd (c,al) -> mkMutInd (c, array_map_left (f l) al)
@@ -727,7 +727,7 @@ let compare_constr f c1 c2 =
| IsProd (_,t1,c1), IsProd (_,t2,c2) -> f t1 t2 & f c1 c2
| IsLambda (_,t1,c1), IsLambda (_,t2,c2) -> f t1 t2 & f c1 c2
| IsLetIn (_,b1,t1,c1), IsLetIn (_,b2,t2,c2) -> f b1 b2 & f t1 t2 & f c1 c2
- | IsAppL (c1,l1), IsAppL (c2,l2) -> f c1 c2 & array_for_all2 f l1 l2
+ | IsApp (c1,l1), IsApp (c2,l2) -> f c1 c2 & array_for_all2 f l1 l2
| IsEvar (e1,l1), IsEvar (e2,l2) -> e1 = e2 & array_for_all2 f l1 l2
| IsConst (c1,l1), IsConst (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
| IsMutInd (c1,l1), IsMutInd (c2,l2) -> c1 = c2 & array_for_all2 f l1 l2
@@ -850,7 +850,7 @@ let noccur_between n m term =
let noccur_with_meta n m term =
let rec occur_rec n c = match kind_of_term c with
| IsRel p -> if n<=p & p<n+m then raise Occur
- | IsAppL(f,cl) ->
+ | IsApp(f,cl) ->
(match kind_of_term f with
| IsCast (c,_) when isMeta c -> ()
| IsMeta _ -> ()
@@ -1072,16 +1072,12 @@ let mkArrow t1 t2 = mkProd (Anonymous, t1, t2)
(* If lt = [t1; ...; tn], constructs the application (t1 ... tn) *)
(* We ensure applicative terms have at most one arguments and the
function is not itself an applicative term *)
-let mkAppL = mkAppL
-
-let mkAppList = function
- | f::l -> mkAppL (f, Array.of_list l)
- | _ -> anomaly "mkAppList received an empty list"
+let mkApp = mkApp
let mkAppA v =
let l = Array.length v in
if l=0 then anomaly "mkAppA received an empty array"
- else mkAppL (v.(0), Array.sub v 1 (Array.length v -1))
+ else mkApp (v.(0), Array.sub v 1 (Array.length v -1))
(* Constructs a constant *)
(* The array of terms correspond to the variables introduced in the section *)
@@ -1190,13 +1186,13 @@ let lamn n env b =
in
lamrec (n,env,b)
-let applist (f,l) = mkAppL (f, Array.of_list l)
+let applist (f,l) = mkApp (f, Array.of_list l)
-let applistc f l = mkAppL (f, Array.of_list l)
+let applistc f l = mkApp (f, Array.of_list l)
-let appvect = mkAppL
+let appvect = mkApp
-let appvectc f l = mkAppL (f,l)
+let appvectc f l = mkApp (f,l)
(* to_lambda n (x1:T1)...(xn:Tn)(xn+1:Tn+1)...(xn+j:Tn+j)T =
* [x1:T1]...[xn:Tn](xn+1:Tn+1)...(xn+j:Tn+j)T *)
@@ -1350,28 +1346,28 @@ let le_kind_implicit k1 k2 =
(* flattens application lists *)
let rec collapse_appl c = match kind_of_term c with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let rec collapse_rec f cl2 = match kind_of_term f with
- | IsAppL (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
- | IsCast (c,_) when isAppL c -> collapse_rec c cl2
- | _ -> if cl2 = [||] then f else mkAppL (f,cl2)
+ | IsApp (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+ | IsCast (c,_) when isApp c -> collapse_rec c cl2
+ | _ -> if cl2 = [||] then f else mkApp (f,cl2)
in
collapse_rec f cl
| _ -> c
let rec decomp_app c =
match kind_of_term (collapse_appl c) with
- | IsAppL (f,cl) -> (f, Array.to_list cl)
+ | IsApp (f,cl) -> (f, Array.to_list cl)
| IsCast (c,t) -> decomp_app c
| _ -> (c,[])
(* strips head casts and flattens head applications *)
let rec strip_head_cast c = match kind_of_term c with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let rec collapse_rec f cl2 = match kind_of_term f with
- | IsAppL (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
+ | IsApp (g,cl1) -> collapse_rec g (Array.append cl1 cl2)
| IsCast (c,_) -> collapse_rec c cl2
- | _ -> if cl2 = [||] then f else mkAppL (f,cl2)
+ | _ -> if cl2 = [||] then f else mkApp (f,cl2)
in
collapse_rec f cl
| IsCast (c,t) -> strip_head_cast c
@@ -1458,7 +1454,7 @@ let rec eta_reduce_head c =
match kind_of_term c with
| IsLambda (_,c1,c') ->
(match kind_of_term (eta_reduce_head c') with
- | IsAppL (f,cl) ->
+ | IsApp (f,cl) ->
let lastn = (Array.length cl) - 1 in
if lastn < 1 then anomaly "application without arguments"
else
@@ -1466,7 +1462,7 @@ let rec eta_reduce_head c =
| IsRel 1 ->
let c' =
if lastn = 1 then f
- else mkAppL (f, Array.sub cl 0 lastn)
+ else mkApp (f, Array.sub cl 0 lastn)
in
if not (dependent (mkRel 1) c')
then lift (-1) c'
@@ -1510,12 +1506,12 @@ let rec rename_bound_var l c =
let prefix_application (k,c) (t : constr) =
let c' = strip_head_cast c and t' = strip_head_cast t in
match kind_of_term c', kind_of_term t' with
- | IsAppL (f1,cl1), IsAppL (f2,cl2) ->
+ | IsApp (f1,cl1), IsApp (f2,cl2) ->
let l1 = Array.length cl1
and l2 = Array.length cl2 in
if l1 <= l2
- && eq_constr c' (mkAppL (f2, Array.sub cl2 0 l1)) then
- Some (mkAppL (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+ && eq_constr c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
else
None
| _ -> None
@@ -1523,12 +1519,12 @@ let prefix_application (k,c) (t : constr) =
let prefix_application_eta (k,c) (t : constr) =
let c' = strip_head_cast c and t' = strip_head_cast t in
match kind_of_term c', kind_of_term t' with
- | IsAppL (f1,cl1), IsAppL (f2,cl2) ->
+ | IsApp (f1,cl1), IsApp (f2,cl2) ->
let l1 = Array.length cl1
and l2 = Array.length cl2 in
if l1 <= l2 &&
- eta_eq_constr c' (mkAppL (f2, Array.sub cl2 0 l1)) then
- Some (mkAppL (mkRel k, Array.sub cl2 l1 (l2 - l1)))
+ eta_eq_constr c' (mkApp (f2, Array.sub cl2 0 l1)) then
+ Some (mkApp (mkRel k, Array.sub cl2 l1 (l2 - l1)))
else
None
| (_,_) -> None
@@ -1700,7 +1696,7 @@ type constr_operator =
| OpSort of sorts
| OpRel of int | OpVar of identifier
| OpCast | OpProd of name | OpLambda of name | OpLetIn of name
- | OpAppL | OpConst of section_path
+ | OpApp | OpConst of section_path
| OpEvar of existential_key
| OpMutInd of inductive_path
| OpMutConstruct of constructor_path
@@ -1717,7 +1713,7 @@ let splay_constr c = match kind_of_term c with
| IsProd (x, t1, t2) -> OpProd x, [|t1;t2|]
| IsLambda (x, t1, t2) -> OpLambda x, [|t1;t2|]
| IsLetIn (x, b, t1, t2) -> OpLetIn x, [|b;t1;t2|]
- | IsAppL (f,a) -> OpAppL, Array.append [|f|] a
+ | IsApp (f,a) -> OpApp, Array.append [|f|] a
| IsConst (sp, a) -> OpConst sp, a
| IsEvar (sp, a) -> OpEvar sp, a
| IsMutInd (ind_sp, l) -> OpMutInd ind_sp, l
@@ -1736,7 +1732,7 @@ let gather_constr = function
| OpProd x, [|t1;t2|] -> mkProd (x, t1, t2)
| OpLambda x, [|t1;t2|] -> mkLambda (x, t1, t2)
| OpLetIn x, [|b;t1;t2|] -> mkLetIn (x, b, t1, t2)
- | OpAppL, v -> let f = v.(0) and a = array_tl v in mkAppL (f, a)
+ | OpApp, v -> let f = v.(0) and a = array_tl v in mkApp (f, a)
| OpConst sp, a -> mkConst (sp, a)
| OpEvar sp, a -> mkEvar (sp, a)
| OpMutInd ind_sp, l -> mkMutInd (ind_sp, l)
@@ -1772,7 +1768,7 @@ let splay_constr_with_binders c = match kind_of_term c with
| IsProd (x, t1, t2) -> OpProd x, [x,None,t1], [|t2|]
| IsLambda (x, t1, t2) -> OpLambda x, [x,None,t1], [|t2|]
| IsLetIn (x, b, t1, t2) -> OpLetIn x, [x,Some b,t1], [|t2|]
- | IsAppL (f,v) -> OpAppL, [], Array.append [|f|] v
+ | IsApp (f,v) -> OpApp, [], Array.append [|f|] v
| IsConst (sp, a) -> OpConst sp, [], a
| IsEvar (sp, a) -> OpEvar sp, [], a
| IsMutInd (ind_sp, l) -> OpMutInd ind_sp, [], l
@@ -1802,7 +1798,7 @@ let gather_constr_with_binders = function
| OpProd _, [x,None,t1], [|t2|] -> mkProd (x, t1, t2)
| OpLambda _, [x,None,t1], [|t2|] -> mkLambda (x, t1, t2)
| OpLetIn _, [x,Some b,t1], [|t2|] -> mkLetIn (x, b, t1, t2)
- | OpAppL, [], v -> let f = v.(0) and a = array_tl v in mkAppL (f, a)
+ | OpApp, [], v -> let f = v.(0) and a = array_tl v in mkApp (f, a)
| OpConst sp, [], a -> mkConst (sp, a)
| OpEvar sp, [], a -> mkEvar (sp, a)
| OpMutInd ind_sp, [], l -> mkMutInd (ind_sp, l)
diff --git a/kernel/term.mli b/kernel/term.mli
index 1994584af..fe26462de 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -116,7 +116,7 @@ type kind_of_term =
| IsProd of name * constr * constr
| IsLambda of name * constr * constr
| IsLetIn of name * constr * constr * constr
- | IsAppL of constr * constr array
+ | IsApp of constr * constr array
| IsEvar of existential
| IsConst of constant
| IsMutInd of inductive
@@ -125,7 +125,7 @@ type kind_of_term =
| IsFix of fixpoint
| IsCoFix of cofixpoint
-(* User view of [constr]. For [IsAppL], it is ensured there is at
+(* User view of [constr]. For [IsApp], it is ensured there is at
least one argument and the function is not itself an applicative
term *)
@@ -197,10 +197,9 @@ val mkNamedLambda : identifier -> constr -> constr -> constr
(* [mkLambda_string s t c] constructs $[s:t]c$ *)
val mkLambda_string : string -> constr -> constr -> constr
-(* [mkAppL (f,[| t_1; ...; t_n |]] constructs the application
+(* [mkApp (f,[| t_1; ...; t_n |]] constructs the application
$(f~t_1~\dots~t_n)$. *)
-val mkAppL : constr * constr array -> constr
-val mkAppList : constr list -> constr
+val mkApp : constr * constr array -> constr
val mkAppA : constr array -> constr
(* Constructs a constant *)
@@ -317,7 +316,7 @@ val destLambda : constr -> name * constr * constr
val destLetIn : constr -> name * constr * constr * constr
(* Destructs an application *)
-val isAppL : constr -> bool
+val isApp : constr -> bool
(*i
val hd_app : constr -> constr
val args_app : constr -> constr array
@@ -365,8 +364,7 @@ val abs_implicit : constr -> constr
val lambda_implicit : constr -> constr
val lambda_implicit_lift : int -> constr -> constr
-(* [applist (f,args)] and co build [mkAppL (f,args)] if [args] non
- empty and build [f] otherwise *)
+(* [applist (f,args)] and co work as [mkApp] *)
val applist : constr * constr list -> constr
val applistc : constr -> constr list -> constr
@@ -561,7 +559,7 @@ type constr_operator =
| OpSort of sorts
| OpRel of int | OpVar of identifier
| OpCast | OpProd of name | OpLambda of name | OpLetIn of name
- | OpAppL | OpConst of section_path
+ | OpApp | OpConst of section_path
| OpEvar of existential_key
| OpMutInd of inductive_path
| OpMutConstruct of constructor_path
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c4e177d44..74b207209 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -616,7 +616,7 @@ let rec check_subterm_rec_meta env sigma vectn k def =
(array_for_all (check_rec_call n lst) la) &&
(List.for_all (check_rec_call n lst) l)
- | IsAppL (f,la) ->
+ | IsApp (f,la) ->
(check_rec_call n lst f) &&
(array_for_all (check_rec_call n lst) la) &&
(List.for_all (check_rec_call n lst) l)
@@ -831,7 +831,7 @@ let control_only_guard env sigma =
| IsMutConstruct (_,cl) -> Array.iter control_rec cl
| IsConst (_,cl) -> Array.iter control_rec cl
| IsEvar (_,cl) -> Array.iter control_rec cl
- | IsAppL (_,cl) -> Array.iter control_rec cl
+ | IsApp (_,cl) -> Array.iter control_rec cl
| IsCast (c1,c2) -> control_rec c1; control_rec c2
| IsProd (_,c1,c2) -> control_rec c1; control_rec c2
| IsLambda (_,c1,c2) -> control_rec c1; control_rec c2
diff --git a/library/indrec.ml b/library/indrec.ml
index 841c2ac38..f96871143 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -100,7 +100,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
let (_,realargs) = list_chop nparams largs in
let base = applist (lift i pk,realargs) in
if depK then
- mkAppL (base, [|appvect (mkRel (i+1),rel_vect 0 i)|])
+ mkApp (base, [|appvect (mkRel (i+1),rel_vect 0 i)|])
else
base
| _ -> assert false
@@ -124,13 +124,13 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
(match optionpos with
| None ->
make_prod env (n,t,process_constr (i+1) c_0 rest
- (mkAppL (lift 1 co, [|mkRel 1|])))
+ (mkApp (lift 1 co, [|mkRel 1|])))
| Some(dep',p) ->
let nP = lift (i+1+decP) p in
let t_0 = process_pos dep' nP (lift 1 t) in
make_prod_dep (dep or dep') env
(n,t,mkArrow t_0 (process_constr (i+2) (lift 1 c_0) rest
- (mkAppL (lift 2 co, [|mkRel 2|])))))
+ (mkApp (lift 2 co, [|mkRel 2|])))))
| IsLetIn (n,b,t,c_0) ->
assert (largs = []);
mkLetIn (n,b,t,process_constr (i+1) c_0 recargs (lift 1 co))
@@ -141,7 +141,7 @@ let type_rec_branch dep env sigma (vargs,depPvect,decP) co t recargs =
| _ -> assert false in
let (_,realargs) = list_chop nparams largs in
let base = applist (nP,realargs) in
- if dep then mkAppL (base, [|co|]) else base
+ if dep then mkApp (base, [|co|]) else base
| _ -> assert false
in
process_constr 0 st recargs (appvect(co,vargs))
diff --git a/parsing/pattern.ml b/parsing/pattern.ml
index 27511b971..176903cb2 100644
--- a/parsing/pattern.ml
+++ b/parsing/pattern.ml
@@ -161,7 +161,7 @@ let matches_core convert pat c =
| PSort RType, IsSort (Type _) -> sigma
- | PApp (c1,arg1), IsAppL (c2,arg2) ->
+ | PApp (c1,arg1), IsApp (c2,arg2) ->
array_fold_left2 (sorec stk) (sorec stk sigma c1 c2) arg1 arg2
| PBinder(BProd,na1,c1,d1), IsProd(na2,c2,d2) ->
@@ -247,14 +247,14 @@ let rec sub_match nocc pat c =
| NextOccurrence nocc ->
let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
(lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
- | IsAppL (c1,lc) ->
+ | IsApp (c1,lc) ->
(try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
| PatternMatchingFailure ->
let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
- (lm,mkAppList le)
+ (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
| NextOccurrence nocc ->
let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
- (lm,mkAppList le))
+ (lm,mkApp (List.hd le, Array.of_list (List.tl le))))
| IsMutCase (ci,hd,c1,lc) ->
(try authorized_occ nocc ((matches pat c), mkMeta (-1)) with
| PatternMatchingFailure ->
@@ -305,7 +305,7 @@ let rec pattern_of_constr t =
PBinder (BProd,na,pattern_of_constr c,pattern_of_constr b)
| IsLambda (na,c,b) ->
PBinder (BLambda,na,pattern_of_constr c,pattern_of_constr b)
- | IsAppL (f,args) ->
+ | IsApp (f,args) ->
PApp (pattern_of_constr f, Array.map pattern_of_constr args)
| IsConst (cst_sp,ctxt) ->
PRef (RConst (cst_sp, ctxt))
diff --git a/parsing/pretty.ml b/parsing/pretty.ml
index b2b0da945..1ae401dc3 100644
--- a/parsing/pretty.ml
+++ b/parsing/pretty.ml
@@ -301,7 +301,7 @@ let print_full_context_typ () = print_context false (Lib.contents_after None)
let rec head_const c = match kind_of_term c with
| IsProd (_,_,d) -> head_const d
| IsLetIn (_,_,_,d) -> head_const d
- | IsAppL (f,_) -> head_const f
+ | IsApp (f,_) -> head_const f
| IsCast (d,_) -> head_const d
| _ -> c
@@ -492,7 +492,7 @@ let unfold_head_fconst =
let rec unfrec k = match kind_of_term k with
| IsConst cst -> constant_value (Global.env ()) cst
| IsLambda (na,t,b) -> mkLambda (na,t,unfrec b)
- | IsAppL (f,v) -> appvect (unfrec f,v)
+ | IsApp (f,v) -> appvect (unfrec f,v)
| _ -> k
in
unfrec
diff --git a/parsing/termast.ml b/parsing/termast.ml
index ca948f9ef..c3608b5ee 100644
--- a/parsing/termast.ml
+++ b/parsing/termast.ml
@@ -29,7 +29,7 @@ let print_arguments = ref false
let print_evar_arguments = ref false
(* This forces printing of cast nodes *)
-let print_casts = ref false
+let print_casts = ref true
(* This governs printing of implicit arguments. When
[print_implicits] is on then [print_implicits_explicit_args] tells
diff --git a/pretyping/class.ml b/pretyping/class.ml
index f9c36315b..b83eb3608 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 d8475e50e..36b5ed4d5 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 2892cddb4..839cfac4f 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 dd3022764..a02cf96a6 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 d3b9c04f6..b877624ad 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 6407284be..b7061962b 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 0bae65053..1e7da4579 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 2c324609a..80948207a 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 b946911e0..8b9319a29 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
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 7271103bc..3e55d555a 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -91,7 +91,7 @@ let unify_0 mc wc m n =
| IsProd (_,t1,c1), IsProd (_,t2,c2) ->
unirec_rec (unirec_rec substn t1 t2) c1 c2
- | IsAppL (f1,l1), IsAppL (f2,l2) ->
+ | IsApp (f1,l1), IsApp (f2,l2) ->
let len1 = Array.length l1
and len2 = Array.length l2 in
if len1 = len2 then
@@ -161,7 +161,7 @@ let whd_castappevar_stack sigma c =
| IsEvar (ev,args) when is_defined sigma ev ->
whrec (existential_value sigma (ev,args), l)
| IsCast (c,_) -> whrec (c, l)
- | IsAppL (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
+ | IsApp (f,args) -> whrec (f, Array.fold_right (fun a l -> a::l) args l)
| _ -> s
in
whrec (c, [])
@@ -244,7 +244,7 @@ and w_resrec metas evars wc =
w_resrec metas t (w_Define evn rhs wc)
with ex when catchable_exception ex ->
(match krhs with
- | IsAppL (f,cl) when isConst f ->
+ | IsApp (f,cl) when isConst f ->
let wc' = mimick_evar f (Array.length cl) evn wc in
w_resrec metas evars wc'
| _ -> error "w_Unify"))
@@ -430,7 +430,7 @@ let clenv_instance_term clenv c =
let clenv_cast_meta clenv =
let rec crec u =
match kind_of_term u with
- | IsAppL _ | IsMutCase _ -> crec_hd u
+ | IsApp _ | IsMutCase _ -> crec_hd u
| IsCast (c,_) when isMeta c -> u
| _ -> map_constr crec u
@@ -445,7 +445,7 @@ let clenv_cast_meta clenv =
| Clval(_) -> u
with Not_found ->
u)
- | IsAppL(f,args) -> mkAppL (crec_hd f, Array.map crec args)
+ | IsApp(f,args) -> mkApp (crec_hd f, Array.map crec args)
| IsMutCase(ci,p,c,br) ->
mkMutCase (ci, crec_hd p, crec_hd c, Array.map crec br)
| _ -> u
@@ -546,7 +546,7 @@ let clenv_merge with_types =
(clenv_wtactic (w_Define evn rhs) clenv)
with ex when catchable_exception ex ->
(match krhs with
- | IsAppL (f,cl) when isConst f or isMutConstruct f ->
+ | IsApp (f,cl) when isConst f or isMutConstruct f ->
clenv_resrec metas evars
(clenv_wtactic
(mimick_evar f (Array.length cl) evn)
@@ -677,10 +677,10 @@ let constrain_clenv_to_subterm clause (op,cl) =
else error "Bound 1"
with ex when catchable_exception ex ->
(match kind_of_term cl with
- | IsAppL (f,args) ->
+ | IsApp (f,args) ->
let n = Array.length args in
assert (n>0);
- let c1 = mkAppL (f,Array.sub args 0 (n-1)) in
+ let c1 = mkApp (f,Array.sub args 0 (n-1)) in
let c2 = args.(n-1) in
(try
matchrec c1
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 77c6a996e..2487d9160 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -69,7 +69,7 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
conv_leq_goal env sigma trm ty conclty;
mk_refgoals sigma goal goalacc ty t
- | IsAppL (f,l) ->
+ | IsApp (f,l) ->
let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
let (acc'',conclty') =
mk_arggoals sigma goal acc' hdty (Array.to_list l) in
@@ -103,7 +103,7 @@ and mk_hdgoals sigma goal goalacc trm =
let ctxt = out_some goal.evar_info in
(mk_goal ctxt env (nf_betaiota env sigma ty))::goalacc,ty
- | IsAppL (f,l) ->
+ | IsApp (f,l) ->
let (acc',hdty) = mk_hdgoals sigma goal goalacc f in
mk_arggoals sigma goal acc' hdty (Array.to_list l)
@@ -148,7 +148,7 @@ let collect_meta_variables c =
let rec collrec acc c = match splay_constr c with
| OpMeta mv, _ -> mv::acc
| OpCast, [|c;_|] -> collrec acc c
- | (OpAppL | OpMutCase _), cl -> Array.fold_left collrec acc cl
+ | (OpApp | OpMutCase _), cl -> Array.fold_left collrec acc cl
| _ -> acc
in
List.rev(collrec [] c)
@@ -157,7 +157,7 @@ let new_meta_variables =
let rec newrec x = match kind_of_term x with
| IsMeta _ -> mkMeta (new_meta())
| IsCast (c,t) -> mkCast (newrec c, t)
- | IsAppL (f,cl) -> appvect (newrec f, Array.map newrec cl)
+ | IsApp (f,cl) -> appvect (newrec f, Array.map newrec cl)
| IsMutCase (ci,p,c,lf) ->
mkMutCase (ci, newrec p, newrec c, Array.map newrec lf)
| _ -> x
diff --git a/tactics/equality.ml b/tactics/equality.ml
index f260604cf..07219dd35 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 d9d81238b..1f78dcb85 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 53cced161..f3bd862a3 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 feb48e4ef..1ed2e536b 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 3f864682e..0c8451870 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 1837b7945..3a1df0234 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-13 05:21:09 +0000