diff options
| author | herbelin | 2001-09-09 15:49:37 +0000 |
|---|---|---|
| committer | herbelin | 2001-09-09 15:49:37 +0000 |
| commit | 14e2cba128e83e7d1289b5d4bb3c702ff3d219b6 (patch) | |
| tree | 28d2869319febd8c650a8e3d1bfc280b4ce974bf /kernel | |
| parent | 382e4f6bb67bec64ea4a0ead5e9de232858a891e (diff) | |
Passage aux univers algébriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1941 85f007b7-540e-0410-9357-904b9bb8a0f7
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 |