diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-14 22:18:47 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-12-14 22:18:47 +0000 |
| commit | ed20a4e9c320ae4bb2f724d181fbb351079d00b2 (patch) | |
| tree | f2c40c77ed55f6da9dff40c8b54e83a5afeaaf24 /kernel/inductive.ml | |
| parent | 910650274c33e28ba71ee8f1194ab9a6db69dfd7 (diff) | |
Les params d'inductif deviennent en même temps propre à chaque inductif d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/inductive.ml')
| -rw-r--r-- | kernel/inductive.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d319f633a..493cb15f5 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -23,7 +23,7 @@ let build_mis ((sp,tyi),args) mib = mis_mip = mind_nth_type_packet mib tyi } let mis_ntypes mis = mis.mis_mib.mind_ntypes -let mis_nparams mis = mis.mis_mib.mind_nparams +let mis_nparams mis = mis.mis_mip.mind_nparams let mis_index mis = mis.mis_tyi @@ -97,7 +97,7 @@ let mis_nf_arity mis = let mis_params_ctxt mispec = let paramsign,_ = - decompose_prod_n_assum mispec.mis_mib.mind_nparams + decompose_prod_n_assum mispec.mis_mip.mind_nparams (body_of_type (mis_nf_arity mispec)) in paramsign |