diff options
| author | herbelin | 2006-06-22 22:17:43 +0000 |
|---|---|---|
| committer | herbelin | 2006-06-22 22:17:43 +0000 |
| commit | a59fe9d45a14c04c0165102c144e4036817e5b03 (patch) | |
| tree | 906d8e090f686b2ccdbe4654657927df500d34a8 /kernel | |
| parent | 5303c048a763d0f9d0b2fd2c14647a78f8157360 (diff) | |
Correction bug du polymorphisme de sort des inductifs (cas où les variables d'univers associées aux arités des paramètres ne sont pas distinctes)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8972 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 12 |
1 files changed, 9 insertions, 3 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index 52f2ea3db7..a6a605d2d2 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -135,16 +135,22 @@ let sort_as_univ = function | Prop Null -> neutral_univ | Prop Pos -> base_univ +let cons_subst u su subst = + try (u, sup su (List.assoc u subst)) :: List.remove_assoc u subst + with Not_found -> (u, su) :: subst + let rec make_subst env exp act = match exp, act with (* Bind expected levels of parameters to actual levels *) | None :: exp, _ :: act -> make_subst env exp act - | Some u :: exp, t :: act -> - (u, sort_as_univ (snd (dest_arity env t))) :: make_subst env exp act + | Some u :: exp, t :: act -> + let su = sort_as_univ (snd (dest_arity env t)) in + cons_subst u su (make_subst env exp act) (* Not enough parameters, create a fresh univ *) | Some u :: exp, [] -> - (u, fresh_local_univ ()) :: make_subst env exp [] + let su = fresh_local_univ () in + cons_subst u su (make_subst env exp []) | None :: exp, [] -> make_subst env exp [] (* Uniform parameters are exhausted *) |