diff options
| author |  mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 22:12:16 +0000 |
|---|---|---|
| committer | mohring <mohring@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2005-11-02 22:12:16 +0000 |
| commit | 2f5c0f8880cd4ccc27cef4980768d35c9ebd26ea (patch) | |
| tree | fb1f33855c930c0f5c46a67529e6df6e24652c9f /contrib/extraction | |
| parent | 30ef31fd8e01d39fb7ce909167dcc1e4a29d7f80 (diff) | |
Types inductifs parametriques
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7493 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'contrib/extraction')
| -rw-r--r-- | contrib/extraction/extraction.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/contrib/extraction/extraction.ml b/contrib/extraction/extraction.ml index 0eb35e95b..55ad52ee2 100644 --- a/contrib/extraction/extraction.ml +++ b/contrib/extraction/extraction.ml @@ -295,8 +295,8 @@ and extract_ind env kn = (* kn is supposed to be in long form *) (* Everything concerning parameters. *) (* We do that first, since they are common to all the [mib]. *) let mip0 = mib.mind_packets.(0) in - let npar = mip0.mind_nparams in - let epar = push_rel_context mip0.mind_params_ctxt env in + let npar = mib.mind_nparams in + let epar = push_rel_context mib.mind_params_ctxt env in (* First pass: we store inductive signatures together with *) (* their type var list. *) let packets = @@ -358,7 +358,7 @@ and extract_ind env kn = (* kn is supposed to be in long form *) | _ -> [] in let field_names = - list_skipn mip0.mind_nparams (names_prod mip0.mind_user_lc.(0)) in + list_skipn mib.mind_nparams (names_prod mip0.mind_user_lc.(0)) in assert (List.length field_names = List.length typ); let projs = ref Cset.empty in let mp,d,_ = repr_kn kn in |