diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:08:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:08:20 +0000 |
| commit | 970b4b750486ad8544b5d0a3b2246282690e6c98 (patch) | |
| tree | d8aeeee6133883547e7e30246fcc544e32ae9746 /kernel/typeops.ml | |
| parent | ca91e3c69ba2dfed3f8fd24f721873f5d0cd2004 (diff) | |
Correction incompatibilites dans la fn des types des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 10 |
1 files changed, 1 insertions, 9 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 74b207209..8421a0543 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -83,15 +83,7 @@ let type_of_constant = Instantiate.constant_type (* Inductive types. *) -(* Q: A faire disparaitre ?? -let instantiate_arity mis = - let ids = ids_of_sign mis.mis_mib.mind_hyps in - let args = Array.to_list mis.mis_args in - let arity = mis.mis_mip.mind_arity in - { body = instantiate_constr ids arity.body args; - typ = arity.typ } -*) -let instantiate_arity = mis_typed_arity +let instantiate_arity = mis_user_arity let type_of_inductive env sigma i = (* TODO: check args *) |