diff options
| author | herbelin | 1999-11-24 17:57:25 +0000 |
|---|---|---|
| committer | herbelin | 1999-11-24 17:57:25 +0000 |
| commit | be800056397163ec9c475e6aee44925c97f86f58 (patch) | |
| tree | 373f85ebce6551ce9c3b4f876715fae44f5736b3 /kernel/typing.ml | |
| parent | a67cb75db8dfd77dceefc8c40960b7e99ff6d302 (diff) | |
MAJ pour fusion avec pretyping
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typing.ml')
| -rw-r--r-- | kernel/typing.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/typing.ml b/kernel/typing.ml index 27b50dceba..db3d00302e 100644 --- a/kernel/typing.ml +++ b/kernel/typing.ml @@ -79,20 +79,20 @@ let rec execute mf env cstr = error "General Fixpoints not allowed"; let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in let fix = mkFix vn i larv lfi vdefv in - check_fix env Evd.empty Spset.empty fix; + check_fix env Evd.empty fix; (make_judge fix larv.(i), cst) | IsCoFix (i,lar,lfi,vdef) -> let (larv,vdefv,cst) = execute_fix mf env lar lfi vdef in let cofix = mkCoFix i larv lfi vdefv in - check_cofix env Evd.empty Spset.empty cofix; + check_cofix env Evd.empty cofix; (make_judge cofix larv.(i), cst) | IsSort (Prop c) -> - (type_of_prop_or_set c, cst0) + (make_judge_of_prop_contents c, cst0) | IsSort (Type u) -> - type_of_type u + make_judge_of_type u | IsAppL (f,args) -> let (j,cst1) = execute mf env f in |