diff options
| -rw-r--r-- | kernel/typeops.ml | 31 | ||||
| -rw-r--r-- | kernel/typeops.mli | 6 | ||||
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 | ||||
| -rw-r--r-- | test-suite/bugs/closed/2996.v | 30 |
6 files changed, 62 insertions, 12 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 98c0dfc20f..cd1f2c8564 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -96,15 +96,22 @@ let judge_of_variable env id = (* Management of context of variables. *) (* Checks if a context of variables can be instantiated by the - variables of the current env *) -(* TODO: check order? *) + variables of the current env. + Order does not have to be checked assuming that all names are distinct *) let check_hyps_inclusion env c sign = Context.fold_named_context - (fun (id,_,ty1) () -> + (fun (id,b1,ty1) () -> try - let ty2 = named_type id env in - if not (eq_constr ty2 ty1) then raise Exit - with Not_found | Exit -> + let (_,b2,ty2) = lookup_named id env in + conv env ty2 ty1; + (match b2,b1 with + | None, None -> () + | None, Some _ -> + (* This is wrong, because we don't know if the body is + needed or not for typechecking: *) () + | Some _, None -> raise NotConvertible + | Some b2, Some b1 -> conv env b2 b1); + with Not_found | NotConvertible | Option.Heterogeneous -> error_reference_variables env id c) sign ~init:() @@ -145,9 +152,17 @@ let type_of_constant_type_knowing_parameters env t paramtyps = mkArity (List.rev ctx,s) let type_of_constant_knowing_parameters env cst paramtyps = + let cb = lookup_constant (fst cst) env in + let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in let ty, cu = constant_type env cst in type_of_constant_type_knowing_parameters env ty paramtyps, cu +let type_of_constant_knowing_parameters_in env cst paramtyps = + let cb = lookup_constant (fst cst) env in + let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in + let ty = constant_type_in env cst in + type_of_constant_type_knowing_parameters env ty paramtyps + let type_of_constant_type env t = type_of_constant_type_knowing_parameters env t [||] @@ -155,13 +170,13 @@ let type_of_constant env cst = type_of_constant_knowing_parameters env cst [||] let type_of_constant_in env cst = + let cb = lookup_constant (fst cst) env in + let _ = check_hyps_inclusion env (mkConstU cst) cb.const_hyps in let ar = constant_type_in env cst in type_of_constant_type_knowing_parameters env ar [||] let judge_of_constant_knowing_parameters env (kn,u as cst) args = let c = mkConstU cst in - let cb = lookup_constant kn env in - let _ = check_hyps_inclusion env c cb.const_hyps in let ty, cu = type_of_constant_knowing_parameters env cst args in let _ = Environ.check_constraints cu env in make_judge c ty diff --git a/kernel/typeops.mli b/kernel/typeops.mli index e6fdf3d6cb..ad0634e6c7 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -120,6 +120,12 @@ val type_of_constant_type_knowing_parameters : val type_of_constant_knowing_parameters : env -> pconstant -> types Lazy.t array -> types constrained +val type_of_constant_knowing_parameters_in : + env -> pconstant -> types Lazy.t array -> types + (** Make a type polymorphic if an arity *) val make_polymorphic_if_constant_for_ind : env -> unsafe_judgment -> constant_type + +(** Check that hyps are included in env and fails with error otherwise *) +val check_hyps_inclusion : env -> constr -> section_context -> unit diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml index 6d7403031a..c8c1d0e213 100644 --- a/pretyping/pretyping.ml +++ b/pretyping/pretyping.ml @@ -311,7 +311,7 @@ let pretype_ref loc evdref env ref us = | ref -> let evd, c = pretype_global loc univ_flexible env !evdref ref us in let () = evdref := evd in - let ty = Retyping.get_type_of env evd c in + let ty = Typing.type_of env evd c in make_judge c ty let judge_of_Type evd s = diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml index aa33c32863..c7bdabe93f 100644 --- a/pretyping/retyping.ml +++ b/pretyping/retyping.ml @@ -183,8 +183,7 @@ let retype ?(polyprop=true) sigma = ~polyprop env (mip,snd ind) argtyps with Reduction.NotArity -> retype_error NotAnArity) | Const cst -> - let t = constant_type_in env cst in - (try Typeops.type_of_constant_type_knowing_parameters env t argtyps + (try Typeops.type_of_constant_knowing_parameters_in env cst argtyps with Reduction.NotArity -> retype_error NotAnArity) | Var id -> type_of_var env id | Construct cstr -> type_of_constructor env cstr diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 92bdd35ecf..669fbfb46e 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -27,7 +27,7 @@ let meta_type evd mv = let constant_type_knowing_parameters env cst jl = let paramstyp = Array.map (fun j -> lazy j.uj_type) jl in - type_of_constant_type_knowing_parameters env (constant_type_in env cst) paramstyp + type_of_constant_knowing_parameters_in env cst paramstyp let inductive_type_knowing_parameters env (ind,u) jl = let mspec = lookup_mind_specif env ind in diff --git a/test-suite/bugs/closed/2996.v b/test-suite/bugs/closed/2996.v new file mode 100644 index 0000000000..440cda6176 --- /dev/null +++ b/test-suite/bugs/closed/2996.v @@ -0,0 +1,30 @@ +(* Test on definitions referring to section variables that are not any + longer in the current context *) + +Section x. + + Hypothesis h : forall(n : nat), n < S n. + + Definition f(n m : nat)(less : n < m) : nat := n + m. + + Lemma a : forall(n : nat), f n (S n) (h n) = 1 + 2 * n. + Proof. + (* XXX *) admit. + Qed. + + Lemma b : forall(n : nat), n < 3 + n. + Proof. + clear. + intros n. + Fail assert (H := a n). + Abort. + + Let T := True. + Definition p := I : T. + + Lemma paradox : False. + Proof. + clear. + set (T := False). + Fail pose proof p as H. + Abort. |