From d44846131cf2fab2d3c45d435b84d802b1af8d43 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 Dec 1999 15:24:13 +0000
Subject: Nouveaux types 'constructor' et 'inductive' dans Term; les fonctions
 sur les inductifs prennent maintenant des 'inductive' en paramètres; elle
 n'ont plus besoin de faire des appels dangereux aux find_m*type qui
 centralisent la levée de raise Induc.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/safe_typing.ml | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

(limited to 'kernel/safe_typing.ml')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2c7829ef94..d7f8b83864 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -57,15 +57,14 @@ let rec execute mf env cstr =
         else 
 	  error "Cannot typecheck an unevaluable abstraction"
 	      
-    | IsConst _ ->
-        (make_judge cstr (type_of_constant env Evd.empty cstr), cst0)
+    | IsConst c ->
+        (make_judge cstr (type_of_constant env Evd.empty c), cst0)
 	  
-    | IsMutInd _ ->
-	(make_judge cstr (type_of_inductive env Evd.empty cstr), cst0)
+    | IsMutInd ind ->
+	(make_judge cstr (type_of_inductive env Evd.empty ind), cst0)
 	  
-    | IsMutConstruct (sp,i,j,args) -> 
-	let (typ,kind) =
-	  destCast (type_of_constructor env Evd.empty (((sp,i),j),args)) in
+    | IsMutConstruct c -> 
+	let (typ,kind) =destCast (type_of_constructor env Evd.empty c) in
         ({ uj_val = cstr; uj_type = typ; uj_kind = kind } , cst0)
 	  
     | IsMutCase (_,p,c,lf) ->
-- 
cgit v1.2.3