diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index d157793e95..dd76eee74c 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -50,8 +50,7 @@ let rec execute env cstr cu = (judge_of_prop_contents c, cu) | IsSort (Type u) -> - let inst_u = if u == dummy_univ then new_univ() else u in - univ_combinator cu (judge_of_type inst_u) + univ_combinator cu (judge_of_type u) | IsApp (f,args) -> let (j,cu1) = execute env f cu in |