diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/closure.ml | 73 | ||||
| -rw-r--r-- | kernel/closure.mli | 23 | ||||
| -rw-r--r-- | kernel/fast_typeops.ml | 6 | ||||
| -rw-r--r-- | kernel/indtypes.ml | 16 | ||||
| -rw-r--r-- | kernel/inductive.ml | 32 | ||||
| -rw-r--r-- | kernel/reduction.ml | 18 | ||||
| -rw-r--r-- | kernel/reduction.mli | 6 | ||||
| -rw-r--r-- | kernel/typeops.ml | 6 |
8 files changed, 109 insertions, 71 deletions
diff --git a/kernel/closure.ml b/kernel/closure.ml index 960bdb649a..817012d8ec 100644 --- a/kernel/closure.ml +++ b/kernel/closure.ml @@ -37,17 +37,20 @@ let delta = ref 0 let eta = ref 0 let zeta = ref 0 let evar = ref 0 -let iota = ref 0 +let nb_match = ref 0 +let fix = ref 0 +let cofix = ref 0 let prune = ref 0 let reset () = - beta := 0; delta := 0; zeta := 0; evar := 0; iota := 0; evar := 0; - prune := 0 + beta := 0; delta := 0; zeta := 0; evar := 0; nb_match := 0; fix := 0; + cofix := 0; evar := 0; prune := 0 let stop() = Feedback.msg_debug (str "[Reds: beta=" ++ int !beta ++ str" delta=" ++ int !delta ++ str " eta=" ++ int !eta ++ str" zeta=" ++ int !zeta ++ str" evar=" ++ - int !evar ++ str" iota=" ++ int !iota ++ str" prune=" ++ int !prune ++ + int !evar ++ str" match=" ++ int !nb_match ++ str" fix=" ++ int !fix ++ + str " cofix=" ++ int !cofix ++ str" prune=" ++ int !prune ++ str"]") let incr_cnt red cnt = @@ -78,7 +81,9 @@ module type RedFlagsSig = sig val fBETA : red_kind val fDELTA : red_kind val fETA : red_kind - val fIOTA : red_kind + val fMATCH : red_kind + val fFIX : red_kind + val fCOFIX : red_kind val fZETA : red_kind val fCONST : constant -> red_kind val fVAR : Id.t -> red_kind @@ -103,14 +108,19 @@ module RedFlags = (struct r_eta : bool; r_const : transparent_state; r_zeta : bool; - r_iota : bool } + r_match : bool; + r_fix : bool; + r_cofix : bool } - type red_kind = BETA | DELTA | ETA | IOTA | ZETA + type red_kind = BETA | DELTA | ETA | MATCH | FIX + | COFIX | ZETA | CONST of constant | VAR of Id.t let fBETA = BETA let fDELTA = DELTA let fETA = ETA - let fIOTA = IOTA + let fMATCH = MATCH + let fFIX = FIX + let fCOFIX = COFIX let fZETA = ZETA let fCONST kn = CONST kn let fVAR id = VAR id @@ -120,7 +130,9 @@ module RedFlags = (struct r_eta = false; r_const = all_opaque; r_zeta = false; - r_iota = false } + r_match = false; + r_fix = false; + r_cofix = false } let red_add red = function | BETA -> { red with r_beta = true } @@ -129,7 +141,9 @@ module RedFlags = (struct | CONST kn -> let (l1,l2) = red.r_const in { red with r_const = l1, Cpred.add kn l2 } - | IOTA -> { red with r_iota = true } + | MATCH -> { red with r_match = true } + | FIX -> { red with r_fix = true } + | COFIX -> { red with r_cofix = true } | ZETA -> { red with r_zeta = true } | VAR id -> let (l1,l2) = red.r_const in @@ -142,7 +156,9 @@ module RedFlags = (struct | CONST kn -> let (l1,l2) = red.r_const in { red with r_const = l1, Cpred.remove kn l2 } - | IOTA -> { red with r_iota = false } + | MATCH -> { red with r_match = false } + | FIX -> { red with r_fix = false } + | COFIX -> { red with r_cofix = false } | ZETA -> { red with r_zeta = false } | VAR id -> let (l1,l2) = red.r_const in @@ -165,7 +181,9 @@ module RedFlags = (struct let c = Id.Pred.mem id l in incr_cnt c delta | ZETA -> incr_cnt red.r_zeta zeta - | IOTA -> incr_cnt red.r_iota iota + | MATCH -> incr_cnt red.r_match nb_match + | FIX -> incr_cnt red.r_fix fix + | COFIX -> incr_cnt red.r_cofix cofix | DELTA -> (* Used for Rel/Var defined in context *) incr_cnt red.r_delta delta @@ -177,15 +195,20 @@ end : RedFlagsSig) open RedFlags -let betadeltaiota = mkflags [fBETA;fDELTA;fZETA;fIOTA] -let betadeltaiotanolet = mkflags [fBETA;fDELTA;fIOTA] -let betaiota = mkflags [fBETA;fIOTA] +let all = mkflags [fBETA;fDELTA;fZETA;fMATCH;fFIX;fCOFIX] +let allnolet = mkflags [fBETA;fDELTA;fMATCH;fFIX;fCOFIX] let beta = mkflags [fBETA] -let betaiotazeta = mkflags [fBETA;fIOTA;fZETA] +let betadeltazeta = mkflags [fBETA;fDELTA;fZETA] +let betaiota = mkflags [fBETA;fMATCH;fFIX;fCOFIX] +let betaiotazeta = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let betazeta = mkflags [fBETA;fZETA] +let delta = mkflags [fDELTA] +let zeta = mkflags [fZETA] +let nored = no_red (* Removing fZETA for finer behaviour would break many developments *) -let unfold_side_flags = [fBETA;fIOTA;fZETA] -let unfold_side_red = mkflags [fBETA;fIOTA;fZETA] +let unfold_side_flags = [fBETA;fMATCH;fFIX;fCOFIX;fZETA] +let unfold_side_red = mkflags [fBETA;fMATCH;fFIX;fCOFIX;fZETA] let unfold_red kn = let flag = match kn with | EvalVarRef id -> fVAR id @@ -896,23 +919,27 @@ let rec knr info m stk = (match ref_value_cache info (RelKey k) with Some v -> kni info v stk | None -> (set_norm m; (m,stk))) - | FConstruct((ind,c),u) when red_set info.i_flags fIOTA -> + | FConstruct((ind,c),u) -> + let use_match = red_set info.i_flags fMATCH in + let use_fix = red_set info.i_flags fFIX in + if use_match || use_fix then (match strip_update_shift_app m stk with - | (depth, args, ZcaseT(ci,_,br,e)::s) -> + | (depth, args, ZcaseT(ci,_,br,e)::s) when use_match -> assert (ci.ci_npar>=0); let rargs = drop_parameters depth ci.ci_npar args in knit info e br.(c-1) (rargs@s) - | (_, cargs, Zfix(fx,par)::s) -> + | (_, cargs, Zfix(fx,par)::s) when use_fix -> let rarg = fapp_stack(m,cargs) in let stk' = par @ append_stack [|rarg|] s in let (fxe,fxbd) = contract_fix_vect fx.term in knit info fxe fxbd stk' - | (depth, args, Zproj (n, m, cst)::s) -> + | (depth, args, Zproj (n, m, cst)::s) when use_match -> let rargs = drop_parameters depth n args in let rarg = project_nth_arg m rargs in kni info rarg s | (_,args,s) -> (m,args@s)) - | FCoFix _ when red_set info.i_flags fIOTA -> + else (m,stk) + | FCoFix _ when red_set info.i_flags fCOFIX -> (match strip_update_shift_app m stk with (_, args, (((ZcaseT _|Zproj _)::_) as stk')) -> let (fxe,fxbd) = contract_fix_vect m.term in diff --git a/kernel/closure.mli b/kernel/closure.mli index 8e172290fb..76145e3f80 100644 --- a/kernel/closure.mli +++ b/kernel/closure.mli @@ -41,8 +41,10 @@ module type RedFlagsSig = sig val fBETA : red_kind val fDELTA : red_kind val fETA : red_kind - (** This flag is never used by the kernel reduction but pretyping does *) - val fIOTA : red_kind + (** The fETA flag is never used by the kernel reduction but pretyping does *) + val fMATCH : red_kind + val fFIX : red_kind + val fCOFIX : red_kind val fZETA : red_kind val fCONST : constant -> red_kind val fVAR : Id.t -> red_kind @@ -73,11 +75,18 @@ end module RedFlags : RedFlagsSig open RedFlags -val beta : reds -val betaiota : reds -val betadeltaiota : reds -val betaiotazeta : reds -val betadeltaiotanolet : reds +(* These flags do not contain eta *) +val all : reds +val allnolet : reds +val beta : reds +val betadeltazeta : reds +val betaiota : reds +val betaiotazeta : reds +val betazeta : reds +val delta : reds +val zeta : reds +val nored : reds + val unfold_side_red : reds val unfold_red : evaluable_global_reference -> reds diff --git a/kernel/fast_typeops.ml b/kernel/fast_typeops.ml index c2c8ee2424..e28d770e8b 100644 --- a/kernel/fast_typeops.ml +++ b/kernel/fast_typeops.ml @@ -35,12 +35,12 @@ let check_constraints cst env = (* This should be a type (a priori without intention to be an assumption) *) let type_judgment env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> {utj_val = c; utj_type = s } | _ -> error_not_type env (make_judge c t) let check_type env c t = - match kind_of_term(whd_betadeltaiota env t) with + match kind_of_term(whd_all env t) with | Sort s -> s | _ -> error_not_type env (make_judge c t) @@ -157,7 +157,7 @@ let judge_of_apply env func funt argsv argstv = let rec apply_rec i typ = if Int.equal i len then typ else - (match kind_of_term (whd_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> let arg = argsv.(i) and argt = argstv.(i) in (try diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index b6942e1334..0b99c8dc23 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -50,7 +50,7 @@ let is_indices_matter () = !indices_matter let weaker_noccur_between env x nvars t = if noccur_between x nvars t then Some t else - let t' = whd_betadeltaiota env t in + let t' = whd_all env t in if noccur_between x nvars t' then Some t' else None @@ -129,7 +129,7 @@ let is_unit constrsinfos = let infos_and_sort env t = let rec aux env t max = - let t = whd_betadeltaiota env t in + let t = whd_all env t in match kind_of_term t with | Prod (name,c1,c2) -> let varj = infer_type env c1 in @@ -409,7 +409,7 @@ let check_correct_par (env,n,ntypes,_) paramdecls ind_index args = | LocalDef _ :: paramdecls -> check param_index (paramdecl_index+1) paramdecls | _::paramdecls -> - match kind_of_term (whd_betadeltaiota env params.(param_index)) with + match kind_of_term (whd_all env params.(param_index)) with | Rel w when Int.equal w paramdecl_index -> check (param_index-1) (paramdecl_index+1) paramdecls | _ -> @@ -436,7 +436,7 @@ if Int.equal nmr 0 then 0 else | (_,[]) -> assert false (* |paramsctxt|>=nmr *) | (lp, LocalDef _ :: paramsctxt) -> find k (index-1) (lp,paramsctxt) | (p::lp,_::paramsctxt) -> - ( match kind_of_term (whd_betadeltaiota env p) with + ( match kind_of_term (whd_all env p) with | Rel w when Int.equal w index -> find (k+1) (index-1) (lp,paramsctxt) | _ -> k) in find 0 (n-1) (lpar,List.rev paramsctxt) @@ -466,7 +466,7 @@ let ienv_push_inductive (env, n, ntypes, ra_env) ((mi,u),lrecparams) = let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -495,7 +495,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( constructor [cn] has a type of the shape [… -> c … -> P], where, more generally, the arrows may be dependent). *) let rec check_pos (env, n, ntypes, ra_env as ienv) nmr c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> let () = assert (List.is_empty largs) in @@ -513,7 +513,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( check_pos (ienv_push_var ienv (na, b, mk_norec)) nmr d) | Rel k -> (try let (ra,rarg) = List.nth ra_env (k-1) in - let largs = List.map (whd_betadeltaiota env) largs in + let largs = List.map (whd_all env) largs in let nmr1 = (match ra with Mrec _ -> compute_rec_par ienv paramsctxt nmr largs @@ -603,7 +603,7 @@ let check_positivity_one ~chkpos recursive (env,_,ntypes,_ as ienv) paramsctxt ( inductive type. *) and check_constructors ienv check_head nmr c = let rec check_constr_rec (env,n,ntypes,ra_env as ienv) nmr lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 8e26370ecf..29966facbf 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -29,20 +29,20 @@ let lookup_mind_specif env (kn,tyi) = (mib, mib.mind_packets.(tyi)) let find_rectype env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match kind_of_term t with | Ind ind -> (ind, l) | _ -> raise Not_found let find_inductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match kind_of_term t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite <> Decl_kinds.CoFinite -> (ind, l) | _ -> raise Not_found let find_coinductive env c = - let (t, l) = decompose_app (whd_betadeltaiota env c) in + let (t, l) = decompose_app (whd_all env c) in match kind_of_term t with | Ind ind when (fst (lookup_mind_specif env (out_punivs ind))).mind_finite == Decl_kinds.CoFinite -> (ind, l) @@ -313,7 +313,7 @@ let check_allowed_sort ksort specif = let is_correct_arity env c pj ind specif params = let arsign,_ = get_instantiated_arity ind specif params in let rec srec env pt ar = - let pt' = whd_betadeltaiota env pt in + let pt' = whd_all env pt in match kind_of_term pt', ar with | Prod (na1,a1,t), (LocalAssum (_,a1'))::ar' -> let () = @@ -323,7 +323,7 @@ let is_correct_arity env c pj ind specif params = (* The last Prod domain is the type of the scrutinee *) | Prod (na1,a1,a2), [] -> (* whnf of t was not needed here! *) let env' = push_rel (LocalAssum (na1,a1)) env in - let ksort = match kind_of_term (whd_betadeltaiota env' a2) with + let ksort = match kind_of_term (whd_all env' a2) with | Sort s -> family_of_sort s | _ -> raise (LocalArity None) in let dep_ind = build_dependent_inductive ind specif params in @@ -563,7 +563,7 @@ let check_inductive_codomain env p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,l' = decompose_app (whd_betadeltaiota env s) in + let i,l' = decompose_app (whd_all env s) in isInd i (* The following functions are almost duplicated from indtypes.ml, except @@ -586,7 +586,7 @@ let ienv_push_inductive (env, ra_env) ((mind,u),lpar) = let rec ienv_decompose_prod (env,_ as ienv) n c = if Int.equal n 0 then (ienv,c) else - let c' = whd_betadeltaiota env c in + let c' = whd_all env c in match kind_of_term c' with Prod(na,a,b) -> let ienv' = ienv_push_var ienv (na,a,mk_norec) in @@ -618,7 +618,7 @@ close to check_positive in indtypes.ml, but does no positivity check and does no compute the number of recursive arguments. *) let get_recargs_approx env tree ind args = let rec build_recargs (env, ra_env as ienv) tree c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> assert (List.is_empty largs); @@ -677,7 +677,7 @@ let get_recargs_approx env tree ind args = and build_recargs_constructors ienv trees c = let rec recargs_constr_rec (env,ra_env as ienv) trees lrec c = - let x,largs = decompose_app (whd_betadeltaiota env c) in + let x,largs = decompose_app (whd_all env c) in match kind_of_term x with | Prod (na,b,d) -> @@ -706,7 +706,7 @@ let restrict_spec env spec p = let env = push_rel_context absctx env in let arctx, s = dest_prod_assum env ar in let env = push_rel_context arctx env in - let i,args = decompose_app (whd_betadeltaiota env s) in + let i,args = decompose_app (whd_all env s) in match kind_of_term i with | Ind i -> begin match spec with @@ -727,7 +727,7 @@ let restrict_spec env spec p = let rec subterm_specif renv stack t = (* maybe reduction is not always necessary! *) - let f,l = decompose_app (whd_betadeltaiota renv.env t) in + let f,l = decompose_app (whd_all renv.env t) in match kind_of_term f with | Rel k -> subterm_var k renv | Case (ci,p,c,lbr) -> @@ -854,11 +854,11 @@ let filter_stack_domain env ci p stack = if noccur_with_meta 1 (Context.Rel.length absctx) ar then stack else let env = push_rel_context absctx env in let rec filter_stack env ar stack = - let t = whd_betadeltaiota env ar in + let t = whd_all env ar in match stack, kind_of_term t with | elt :: stack', Prod (n,a,c0) -> let d = LocalAssum (n,a) in - let ty, args = decompose_app (whd_betadeltaiota env a) in + let ty, args = decompose_app (whd_all env a) in let elt = match kind_of_term ty with | Ind ind -> let spec' = stack_element_specif elt in @@ -1047,7 +1047,7 @@ let inductive_of_mutfix env ((nvect,bodynum),(names,types,bodies as recdef)) = (* check fi does not appear in the k+1 first abstractions, gives the type of the k+1-eme abstraction (must be an inductive) *) let rec check_occur env n def = - match kind_of_term (whd_betadeltaiota env def) with + match kind_of_term (whd_all env def) with | Lambda (x,a,b) -> if noccur_with_meta n nbfix a then let env' = push_rel (LocalAssum (x,a)) env in @@ -1101,7 +1101,7 @@ let anomaly_ill_typed () = anomaly ~label:"check_one_cofix" (Pp.str "too many arguments applied to constructor") let rec codomain_is_coind env c = - let b = whd_betadeltaiota env c in + let b = whd_all env c in match kind_of_term b with | Prod (x,a,b) -> codomain_is_coind (push_rel (LocalAssum (x,a)) env) b @@ -1113,7 +1113,7 @@ let rec codomain_is_coind env c = let check_one_cofix env nbfix def deftype = let rec check_rec_call env alreadygrd n tree vlra t = if not (noccur_with_meta n nbfix t) then - let c,args = decompose_app (whd_betadeltaiota env t) in + let c,args = decompose_app (whd_all env t) in match kind_of_term c with | Rel p when n <= p && p < n+nbfix -> (* recursive call: must be guarded and no nested recursive diff --git a/kernel/reduction.ml b/kernel/reduction.ml index 710bfa19b8..2dc2f0c7c9 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -107,17 +107,17 @@ let whd_betaiotazeta env x = Prod _|Lambda _|Fix _|CoFix _) -> x | _ -> whd_val (create_clos_infos betaiotazeta env) (inject x) -let whd_betadeltaiota env t = +let whd_all env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _) -> t - | _ -> whd_val (create_clos_infos betadeltaiota env) (inject t) + | _ -> whd_val (create_clos_infos all env) (inject t) -let whd_betadeltaiota_nolet env t = +let whd_allnolet env t = match kind_of_term t with | (Sort _|Meta _|Evar _|Ind _|Construct _| Prod _|Lambda _|Fix _|CoFix _|LetIn _) -> t - | _ -> whd_val (create_clos_infos betadeltaiotanolet env) (inject t) + | _ -> whd_val (create_clos_infos allnolet env) (inject t) (********************************************************************) (* Conversion *) @@ -731,7 +731,7 @@ let betazeta_appvect = lambda_appvect_assum * error message. *) let hnf_prod_app env t n = - match kind_of_term (whd_betadeltaiota env t) with + match kind_of_term (whd_all env t) with | Prod (_,_,b) -> subst1 n b | _ -> anomaly ~label:"hnf_prod_app" (Pp.str "Need a product") @@ -742,7 +742,7 @@ let hnf_prod_applist env t nl = let dest_prod env = let rec decrec env m c = - let t = whd_betadeltaiota env c in + let t = whd_all env c in match kind_of_term t with | Prod (n,a,c0) -> let d = LocalAssum (n,a) in @@ -754,7 +754,7 @@ let dest_prod env = (* The same but preserving lets in the context, not internal ones. *) let dest_prod_assum env = let rec prodec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match kind_of_term rty with | Prod (x,t,c) -> let d = LocalAssum (x,t) in @@ -764,7 +764,7 @@ let dest_prod_assum env = prodec_rec (push_rel d env) (Context.Rel.add d l) c | Cast (c,_,_) -> prodec_rec env l c | _ -> - let rty' = whd_betadeltaiota env rty in + let rty' = whd_all env rty in if Term.eq_constr rty' rty then l, rty else prodec_rec env l rty' in @@ -772,7 +772,7 @@ let dest_prod_assum env = let dest_lam_assum env = let rec lamec_rec env l ty = - let rty = whd_betadeltaiota_nolet env ty in + let rty = whd_allnolet env ty in match kind_of_term rty with | Lambda (x,t,c) -> let d = LocalAssum (x,t) in diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 3896446925..9812c45f7b 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -12,9 +12,11 @@ open Environ (*********************************************************************** s Reduction functions *) +(* None of these functions do eta reduction *) + val whd_betaiotazeta : env -> constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr val whd_betaiota : env -> constr -> constr val nf_betaiota : env -> constr -> constr diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 0ea68e2bcc..683f6bde55 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -37,7 +37,7 @@ let check_constraints cst env = (* This should be a type (a priori without intension to be an assumption) *) let type_judgment env j = - match kind_of_term(whd_betadeltaiota env j.uj_type) with + match kind_of_term(whd_all env j.uj_type) with | Sort s -> {utj_val = j.uj_val; utj_type = s } | _ -> error_not_type env j @@ -137,7 +137,7 @@ let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} = let params, ccl = dest_prod_assum env t in match kind_of_term ccl with | Sort (Type u) -> - let ind, l = decompose_app (whd_betadeltaiota env c) in + let ind, l = decompose_app (whd_all env c) in if isInd ind && List.is_empty l then let mis = lookup_mind_specif env (fst (destInd ind)) in let nparams = Inductive.inductive_params mis in @@ -233,7 +233,7 @@ let judge_of_apply env funj argjv = { uj_val = mkApp (j_val funj, Array.map j_val argjv); uj_type = typ } | hj::restjl -> - (match kind_of_term (whd_betadeltaiota env typ) with + (match kind_of_term (whd_all env typ) with | Prod (_,c1,c2) -> (try let () = conv_leq false env hj.uj_type c1 in |