From be800056397163ec9c475e6aee44925c97f86f58 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 24 Nov 1999 17:57:25 +0000
Subject: MAJ pour fusion avec pretyping

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@138 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/typing.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'kernel/typing.ml')

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
-- 
cgit v1.2.3