From 405f26bc8d074461f1f87e85d17402002c2f3758 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Tue, 6 Jan 2015 20:18:42 +0100 Subject: Fix checker's treatment of template polymorphic inductive instantiation, now using substitution of levels. Fixes the test-suite file coqchk/univ. --- checker/inductive.ml | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) (limited to 'checker/inductive.ml') diff --git a/checker/inductive.ml b/checker/inductive.ml index c95cb7a2e..68cea38e7 100644 --- a/checker/inductive.ml +++ b/checker/inductive.ml @@ -143,10 +143,7 @@ let sort_as_univ = function | Prop Pos -> Univ.type0_univ let cons_subst u su subst = - try - (u, Univ.sup su (List.assoc_f Univ.Level.equal u subst)) :: - List.remove_assoc_f Univ.Level.equal u subst - with Not_found -> (u, su) :: subst + Univ.LMap.add u su subst let actualize_decl_level env lev t = let sign,s = dest_arity env t in @@ -179,15 +176,10 @@ let rec make_subst env = function (* (actualize_decl_level), then to the conclusion of the arity (via *) (* the substitution) *) let ctx,subst = make_subst env (sign, exp, []) in - (* if polymorphism_on_non_applied_parameters then *) - (* let s = fresh_local_univ () in *) - (* let t = actualize_decl_level env (Type s) t in *) - (* (na,None,t)::ctx, cons_subst u s subst *) - (* else *) d::ctx, subst | sign, [], _ -> (* Uniform parameters are exhausted *) - sign,[] + sign,Univ.LMap.empty | [], _, _ -> assert false @@ -197,7 +189,7 @@ exception SingletonInductiveBecomesProp of Id.t let instantiate_universes env ctx ar argsorts = let args = Array.to_list argsorts in let ctx,subst = make_subst env (ctx,ar.template_param_levels,args) in - let level = Univ.subst_large_constraints subst ar.template_level in + let level = Univ.subst_univs_universe (Univ.make_subst subst) ar.template_level in let ty = (* Singleton type not containing types are interpretable in Prop *) if Univ.is_type0m_univ level then Prop Null -- cgit v1.2.3