diff options
| -rw-r--r-- | pretyping/typing.ml | 19 | ||||
| -rw-r--r-- | proofs/tacmach.ml | 3 | ||||
| -rw-r--r-- | test-suite/success/hyps_inclusion.v | 32 |
3 files changed, 49 insertions, 5 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index d248ba70e..72095e6c4 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -29,6 +29,15 @@ let meta_type env mv = let vect_lift = Array.mapi lift let vect_lift_type = Array.mapi (fun i t -> type_app (lift i) t) +let constant_type_knowing_parameters env cst jl = + let paramstyp = Array.map (fun j -> j.uj_type) jl in + type_of_constant_knowing_parameters env (constant_type env cst) paramstyp + +let inductive_type_knowing_parameters env ind jl = + let (mib,mip) = lookup_mind_specif env ind in + let paramstyp = Array.map (fun j -> j.uj_type) jl in + Inductive.type_of_inductive_knowing_parameters env mip paramstyp + (* The typing machine without information, without universes but with existential variables. *) @@ -93,12 +102,14 @@ let rec execute env evd cstr = match kind_of_term f with | Ind ind -> (* Sort-polymorphism of inductive types *) - judge_of_inductive_knowing_parameters env ind - (jv_nf_evar (evars_of evd) jl) + make_judge f + (inductive_type_knowing_parameters env ind + (jv_nf_evar (evars_of evd) jl)) | Const cst -> (* Sort-polymorphism of inductive types *) - judge_of_constant_knowing_parameters env cst - (jv_nf_evar (evars_of evd) jl) + make_judge f + (constant_type_knowing_parameters env cst + (jv_nf_evar (evars_of evd) jl)) | _ -> execute env evd f in diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml index adb18daa7..06178324d 100644 --- a/proofs/tacmach.ml +++ b/proofs/tacmach.ml @@ -102,6 +102,7 @@ let pf_nf_betaiota = pf_reduce (fun _ _ -> nf_betaiota) let pf_compute = pf_reduce compute let pf_unfoldn ubinds = pf_reduce (unfoldn ubinds) let pf_type_of = pf_reduce type_of +let pf_get_type_of = pf_reduce Retyping.get_type_of let pf_conv_x = pf_reduce is_conv let pf_conv_x_leq = pf_reduce is_conv_leq @@ -109,7 +110,7 @@ let pf_const_value = pf_reduce (fun env _ -> constant_value env) let pf_reduce_to_quantified_ind = pf_reduce reduce_to_quantified_ind let pf_reduce_to_atomic_ind = pf_reduce reduce_to_atomic_ind -let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_type_of gls) +let hnf_type_of gls = compose (pf_whd_betadeltaiota gls) (pf_get_type_of gls) let pf_check_type gls c1 c2 = ignore (pf_type_of gls (mkCast (c1, DEFAULTcast, c2))) diff --git a/test-suite/success/hyps_inclusion.v b/test-suite/success/hyps_inclusion.v new file mode 100644 index 000000000..21bfc0758 --- /dev/null +++ b/test-suite/success/hyps_inclusion.v @@ -0,0 +1,32 @@ +(* Simplified example for bug #1325 *) + +(* Explanation: the proof engine see section variables as goal + variables; especially, it can change their types so that, at + type-checking, the section variables are not recognized + (Typeops.check_hyps_inclusion raises "types do no match"). It + worked before the introduction of polymorphic inductive types because + tactics were using Typing.type_of and not Typeops.typing; the former + was not checking hyps inclusion so that the discrepancy in the types + of section variables seen as goal variables was not a problem (at the + end, when the proof is completed, the section variable recovers its + original type and all is correct for Typeops) *) + +Section A. +Variable H:not True. +Lemma f:nat->nat. destruct H. exact I. Defined. +Goal f 0=f 1. +red in H. +(* next tactic was failing wrt bug #1325 because type-checking the goal + detected a syntactically different type for the section variable H *) +case 0. +Reset A. + +(* Variant with polymorphic inductive types for bug #1325 *) + +Section A. +Variable H:not True. +Inductive I (n:nat) : Type := C : H=H -> I n. +Goal I 0. +red in H. +case 0. +Reset A. |