diff options
| author | sacerdot | 2005-01-14 14:30:06 +0000 |
|---|---|---|
| committer | sacerdot | 2005-01-14 14:30:06 +0000 |
| commit | b5657ff1939c6872ee3ccaeaf180a2f3da9e1876 (patch) | |
| tree | 329838825dc03d431fc36489fdc818ca04d4bd2a /kernel/indtypes.ml | |
| parent | 6dbc9f181b90216958fd9d87f8426901b1e4c37e (diff) | |
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
to accept a mind_specif (a couple mutual_inductive_body * one_inductive_body)
instead of looking it up in the environment. A version of the same functions
with the old type is put in Inductiveops (outside the kernel).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6589 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 5f9f907f52..5aee04f7d7 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -317,9 +317,10 @@ let ienv_push_var (env, n, ntypes, lra) (x,a,ra) = let ienv_push_inductive (env, n, ntypes, ra_env) (mi,lpar) = let auxntyp = 1 in + let specif = lookup_mind_specif env mi in let env' = push_rel (Anonymous,None, - hnf_prod_applist env (type_of_inductive env mi) lpar) env in + hnf_prod_applist env (type_of_inductive specif) lpar) env in let ra_env' = (Imbr mi,Rtree.mk_param 0) :: List.map (fun (r,t) -> (r,Rtree.lift 1 t)) ra_env in |