diff options
| author | Hugo Herbelin | 2014-06-28 17:13:22 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2014-06-28 18:55:31 +0200 |
| commit | cad44fcfe8a129af24d4d9d1f86c8be123707744 (patch) | |
| tree | 437271cc203c9725f7f5045b6c6e032183047141 /pretyping | |
| parent | 1f0e44c96872196d0051618de77c4735eb447540 (diff) | |
Quickly fixing bug #2996: typing functions now check when referring to
a global reference that the current (goal) env contains all the
section variables that the global reference expects to be present.
Note that the test for inclusion might be costly: everytime a
conversion happens in a section variable copied in a goal, this
conversion has to be redone when referring to a constant dependent on
this section variable.
It is unclear to me whether we should not instead give global names to
section variables so that they exist even if they are not listed in
the context of the current goal.
Here are two examples which are still problematic:
Section A.
Let B := True : Type.
Definition C := eq_refl : B = True.
Theorem D : Type.
clearbody B.
set (x := C).
unfold C in x.
(* inconsistent context *)
or
Section A.
Let B : Type.
exact True.
Qed.
Definition C := eq_refl : B = True. (* Note that this violated the Qed. *)
Theorem D : Type.
set (x := C).
unfold C in x.
(* inconsistent context *)
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/pretyping.ml | 2 | ||||
| -rw-r--r-- | pretyping/retyping.ml | 3 | ||||
| -rw-r--r-- | pretyping/typing.ml | 2 |
3 files changed, 3 insertions, 4 deletions
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 |