diff options
Diffstat (limited to 'pretyping/typing.ml')
| -rw-r--r-- | pretyping/typing.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/pretyping/typing.ml b/pretyping/typing.ml index 3f0ab9501a..8279fb7e89 100644 --- a/pretyping/typing.ml +++ b/pretyping/typing.ml @@ -95,7 +95,8 @@ let rec execute mf env sigma cstr = let varj = type_judgment env sigma j in let env1 = push_rel_assum (name,varj.utj_val) env in let j' = execute mf env1 sigma c2 in - let (j,_) = gen_rel env1 sigma name varj j' in + let varj' = type_judgment env sigma j' in + let (j,_) = gen_rel env1 sigma name varj varj' in j | IsLetIn (name,c1,c2,c3) -> |