From 40183da6b54d8deef242bac074079617d4a657c2 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Fri, 21 Jan 2000 18:42:22 +0000
Subject: gros commit de tout ce que j'ai fait pendant les vacances :  -
 tactics/Equality  - debug du discharge  - constr_of_compattern implante vite
 fait / mal fait en attendant mieux  - theories/Logic (ne passe pas
 entierrement)

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

(limited to 'kernel/typeops.ml')

diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1254d5ef99..4b20f3b0a9 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -84,7 +84,7 @@ let check_hyps id env sigma hyps =
 let type_of_constant env sigma (sp,args) =
   let cb = lookup_constant sp env in
   let hyps = cb.const_hyps in
-  check_hyps (basename sp) env sigma hyps;
+  (* TODO: check args *)
   instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
 
 (* Inductive types. *)
@@ -99,7 +99,7 @@ let instantiate_arity mis =
 let type_of_inductive env sigma i =
   let mis = lookup_mind_specif i env in
   let hyps = mis.mis_mib.mind_hyps in
-  check_hyps (basename mis.mis_sp) env sigma hyps;
+  (* TODO: check args *)
   instantiate_arity mis
 
 (* Constructors. *)
@@ -112,7 +112,7 @@ let instantiate_lc mis =
 let type_of_constructor env sigma ((ind_sp,j),args as cstr) =
   let mind = inductive_of_constructor cstr in
   let mis = lookup_mind_specif mind env in
-  check_hyps (basename mis.mis_sp) env sigma (mis.mis_mib.mind_hyps);
+  (* TODO: check args *)
   let specif = instantiate_lc mis in
   let make_ik k = DOPN (MutInd (mis.mis_sp,k), mis.mis_args) in
   if j > mis_nconstr mis then
@@ -161,7 +161,7 @@ let type_of_existential env sigma c =
   let evi = Evd.map sigma ev in
   let hyps = var_context evi.Evd.evar_env in
   let id = id_of_string ("?" ^ string_of_int ev) in
-  check_hyps id env sigma hyps;
+  (* TODO: check args *)
   instantiate_constr (ids_of_sign hyps) evi.Evd.evar_concl (Array.to_list args)
 
 
-- 
cgit v1.2.3