Merge branch 'v8.5'

5 files changed, 24 insertions, 24 deletions

diff --git a/kernel/cbytecodes.ml b/kernel/cbytecodes.ml
index 891d95378..448bf8544 100644
--- a/kernel/cbytecodes.ml
+++ b/kernel/cbytecodes.ml
@@ -17,13 +17,16 @@ open Term
 
 type tag = int
 
-let id_tag = 0
-let iddef_tag = 1
-let ind_tag = 2
-let fix_tag = 3
+let accu_tag = 0
+
+let max_atom_tag = 1
+let proj_tag = 2
+let fix_app_tag = 3
 let switch_tag = 4
 let cofix_tag = 5
 let cofix_evaluated_tag = 6
+
+
 (* It would be great if OCaml exported this value,
    So fixme if this happens in a new version of OCaml *)
 let last_variant_tag = 245 
diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
index 8f594a45b..03d638305 100644
--- a/kernel/cbytecodes.mli
+++ b/kernel/cbytecodes.mli
@@ -13,13 +13,15 @@ open Term
 
 type tag = int
 
-val id_tag : tag
-val iddef_tag : tag
-val ind_tag : tag
-val fix_tag : tag
+val accu_tag : tag
+
+val max_atom_tag : tag
+val proj_tag : tag
+val fix_app_tag : tag
 val switch_tag : tag
 val cofix_tag : tag
 val cofix_evaluated_tag : tag
+
 val last_variant_tag : tag 
 
 type structured_constant =
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index a02d5e205..1f8706652 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -165,10 +165,7 @@ let rec make_subst env =
         (* to be greater than the level of the argument; this is probably *)
         (* a useless extra constraint *)
         let s = sort_as_univ (snd (dest_arity env (Lazy.force a))) in
-	  if Univ.Universe.is_levels s then
-            make (cons_subst u s subst) (sign, exp, args)
-	  else (* Cannot handle substitution by i+n universes. *)
-	    make subst (sign, exp, args)
+          make (cons_subst u s subst) (sign, exp, args)
     | (na,None,t)::sign, Some u::exp, [] ->
         (* No more argument here: we add the remaining universes to the *)
         (* substitution (when [u] is distinct from all other universes in the *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index fe82d85d5..8895bae5d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -134,10 +134,16 @@ let extract_context_levels env l =
 let make_polymorphic_if_constant_for_ind env {uj_val = c; uj_type = t} =
   let params, ccl = dest_prod_assum env t in
   match kind_of_term ccl with
-  | Sort (Type u) when isInd (fst (decompose_app (whd_betadeltaiota env c))) ->
-      let param_ccls = extract_context_levels env params in
-      let s = { template_param_levels = param_ccls; template_level = u} in
-      TemplateArity (params,s)
+  | Sort (Type u) ->
+     let ind, l = decompose_app (whd_betadeltaiota env c) in
+     if isInd ind && List.is_empty l then
+       let mis = lookup_mind_specif env (fst (destInd ind)) in
+       let nparams = Inductive.inductive_params mis in
+       let paramsl = CList.lastn nparams params in
+       let param_ccls = extract_context_levels env paramsl in
+       let s = { template_param_levels = param_ccls; template_level = u} in
+       TemplateArity (params,s)
+     else RegularArity t
   | _ ->
       RegularArity t
 
diff --git a/kernel/vm.ml b/kernel/vm.ml
index 29e2ee601..eacd803fd 100644
--- a/kernel/vm.ml
+++ b/kernel/vm.ml
@@ -19,14 +19,6 @@ external set_drawinstr : unit -> unit = "coq_set_drawinstr"
 external offset_closure : Obj.t -> int -> Obj.t = "coq_offset_closure"
 external offset : Obj.t -> int = "coq_offset"
 
-let accu_tag = 0
-let max_atom_tag = 1
-let proj_tag = 2
-let fix_app_tag = 3
-let switch_tag = 4
-let cofix_tag = 5
-let cofix_evaluated_tag = 6
-
 (*******************************************)
 (* Initalization of the abstract machine ***)
 (*******************************************)