diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/inductive.ml | 14 |
1 files changed, 10 insertions, 4 deletions
diff --git a/kernel/inductive.ml b/kernel/inductive.ml index d9f9f912..76553237 100644 --- a/kernel/inductive.ml +++ b/kernel/inductive.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: inductive.ml 8871 2006-05-28 16:46:48Z herbelin $ *) +(* $Id: inductive.ml 8972 2006-06-22 22:17:43Z herbelin $ *) open Util open Names @@ -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 *) |