From e583a79b5a0298fd08f34305cc876d5117913e95 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 21 Nov 2015 00:23:12 +0100 Subject: Fixing kernel bug in typing match with let-ins in the arity. Was exploitable in 8.3, 8.4 and 8.5beta1. A priori not exploitable in 8.5beta2 and 8.5beta3 from a Coq file because typing done while compiling "match" would serve as a protection. However exploitable by calling the kernel directly, e.g. from a plugin (but a plugin can anyway do what it wants by bypassing kernel type abstraction). Fixing similar error in pretyping. --- pretyping/reductionops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml index 156c9a2772..bdd9ed81cf 100644 --- a/pretyping/reductionops.ml +++ b/pretyping/reductionops.ml @@ -1651,7 +1651,7 @@ let betazetaevar_applist sigma n c l = if Int.equal n 0 then applist (substl env t, stack) else match kind_of_term t, stack with | Lambda(_,_,c), arg::stacktl -> stacklam (n-1) (arg::env) c stacktl - | LetIn(_,b,_,c), _ -> stacklam (n-1) (b::env) c stack + | LetIn(_,b,_,c), _ -> stacklam (n-1) (substl env b::env) c stack | Evar ev, _ -> (match safe_evar_value sigma ev with | Some body -> stacklam n env body stack -- cgit v1.2.3 From af954522789043202d9c300a0bb37cbaf4958d60 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 17:17:49 +0100 Subject: Fixing a bug of adjust_subst_to_rel_context. --- pretyping/termops.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/termops.ml b/pretyping/termops.ml index 5a55d47fd1..ebd9d939aa 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -930,7 +930,7 @@ let adjust_subst_to_rel_context sign l = match sign, l with | (_,None,_)::sign', a::args' -> aux (a::subst) sign' args' | (_,Some c,_)::sign', args' -> - aux (substl (List.rev subst) c :: subst) sign' args' + aux (substl subst c :: subst) sign' args' | [], [] -> List.rev subst | _ -> anomaly (Pp.str "Instance and signature do not match") in aux [] (List.rev sign) l -- cgit v1.2.3 From c4e2cf027b3fade4f9c2806e6061e1294a99e540 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sun, 22 Nov 2015 21:17:59 +0100 Subject: Fixing a vm_compute bug in the presence of let-ins among the parameters of an inductive type. --- pretyping/vnorm.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'pretyping') diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml index c4c85a62ed..be772a6677 100644 --- a/pretyping/vnorm.ml +++ b/pretyping/vnorm.ml @@ -59,11 +59,12 @@ let type_constructor mind mib u typ params = let s = ind_subst mind mib u in let ctyp = substl s typ in let ctyp = subst_instance_constr u ctyp in - let nparams = Array.length params in - if Int.equal nparams 0 then ctyp + let ndecls = Context.rel_context_length mib.mind_params_ctxt in + if Int.equal ndecls 0 then ctyp else - let _,ctyp = decompose_prod_n nparams ctyp in - substl (Array.rev_to_list params) ctyp + let _,ctyp = decompose_prod_n_assum ndecls ctyp in + substl (List.rev (Termops.adjust_subst_to_rel_context mib.mind_params_ctxt (Array.to_list params))) + ctyp -- cgit v1.2.3 From 1467c22548453cd07ceba0029e37c8bbdfd039ea Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Mon, 23 Nov 2015 17:51:16 +0100 Subject: Fixing an old typo in Retyping, found by Matej. --- pretyping/retyping.ml | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) (limited to 'pretyping') diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index fb55265526..a169a4577e 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -158,8 +158,7 @@ let retype ?(polyprop=true) sigma = and sort_family_of env t = match kind_of_term t with | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) - | Sort (Prop c) -> InType - | Sort (Type u) -> InType + | Sort s -> family_of_sort s | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (name,None,t) env) c2 in if not (is_impredicative_set env) && -- cgit v1.2.3 From e92aeed3abcf7d42045deb9fb3a450d3527eadc9 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Wed, 25 Nov 2015 17:33:24 +0100 Subject: Reverting 1467c225 (Fixing an old typo in Retyping, found by Matej). This was not a typo (was correctly taking the family type of the type). --- pretyping/retyping.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping') diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index a169a4577e..fb55265526 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -158,7 +158,8 @@ let retype ?(polyprop=true) sigma = and sort_family_of env t = match kind_of_term t with | Cast (c,_, s) when isSort s -> family_of_sort (destSort s) - | Sort s -> family_of_sort s + | Sort (Prop c) -> InType + | Sort (Type u) -> InType | Prod (name,t,c2) -> let s2 = sort_family_of (push_rel (name,None,t) env) c2 in if not (is_impredicative_set env) && -- cgit v1.2.3