diff options
| author | herbelin | 2001-02-14 15:41:55 +0000 |
|---|---|---|
| committer | herbelin | 2001-02-14 15:41:55 +0000 |
| commit | e7d592ada2d681876d2bcf0a45d4267b3746064f (patch) | |
| tree | e0b7eb1e67b1871b7cb356c33f66182f6dde86c3 /kernel/typeops.ml | |
| parent | 045c85f66a65c6aaedeed578d352c6de27d5e6a4 (diff) | |
Mise en place d'un système optionnel de discharge immédiat; prise en compte des défs locales dans les arguments des inductifs; nettoyage divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 13 |
1 files changed, 4 insertions, 9 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index ae1bb46cfa..fa3db0b86e 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -78,21 +78,16 @@ let type_of_constant = Instantiate.constant_type (* Inductive types. *) -let instantiate_arity = mis_user_arity - let type_of_inductive env sigma i = (* TODO: check args *) - instantiate_arity (lookup_mind_specif i env) + mis_arity (lookup_mind_specif i env) (* Constructors. *) -let type_mconstruct env sigma i mind = - mis_type_mconstruct i (lookup_mind_specif mind env) - let type_of_constructor env sigma cstr = - type_mconstruct env sigma - (index_of_constructor cstr) - (inductive_of_constructor cstr) + mis_constructor_type + (index_of_constructor cstr) + (lookup_mind_specif (inductive_of_constructor cstr) env) let type_of_existential env sigma ev = Instantiate.existential_type sigma ev |