Fix checker's treatment of template polymorphic

inductive instantiation, now using substitution of levels.
Fixes the test-suite file coqchk/univ.

3 files changed, 3 insertions, 35 deletions

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
diff --git a/checker/univ.ml b/checker/univ.ml
index dd048cb2f..73c292508 100644
--- a/checker/univ.ml
+++ b/checker/univ.ml
@@ -1016,25 +1016,6 @@ let check_constraints c g =
   Constraint.for_all (check_constraint g) c
 
 (**********************************************************************)
-(* Tools for sort-polymorphic inductive types                         *)
-
-(* Miscellaneous functions to remove or test local univ assumed to
-   occur only in the le constraints *)
-
-let remove_large_constraint u v min = 
-  match Universe.level v with
-  | Some u' -> if Level.equal u u' then min else v
-  | None -> Huniv.remove (Universe.Expr.make u) v
-
-let subst_large_constraint u u' v =
-  (* if is_direct_constraint u v then  *)
-  Universe.sup u' (remove_large_constraint u v type0m_univ)
-  (* else v *)
-
-let subst_large_constraints =
-  List.fold_right (fun (u,u') -> subst_large_constraint u u')
-
-(**********************************************************************)
 (** Universe polymorphism                                             *)
 (**********************************************************************)
 
diff --git a/checker/univ.mli b/checker/univ.mli
index a4a3a9cb1..479b44523 100644
--- a/checker/univ.mli
+++ b/checker/univ.mli
@@ -120,11 +120,6 @@ val merge_constraints : constraints -> universes -> universes
 
 val check_constraints : constraints -> universes -> bool
 
-(** {6 Support for old-style sort-polymorphism } *)
-
-val subst_large_constraints :
-  (universe_level * universe) list -> universe -> universe
-
 (** {6 Support for universe polymorphism } *)
 
 (** Polymorphic maps from universe levels to 'a *)