- Fix handling of polymorphic inductive elimination schemes.

- Avoid generation of dummy universes for unsafe_global*
- Handle side effects better for polymorphic definitions.

Conflicts:
	kernel/term_typing.ml
	tactics/tactics.ml

2 files changed, 27 insertions, 8 deletions

diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 7c5b8c7283..27ab90aa59 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -70,20 +70,39 @@ let handle_side_effects env body side_eff =
     let rec sub c i x = match kind_of_term x with
       | Const (c', _) when eq_constant c c' -> mkRel i
       | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub c i x) i x in
+    let rec sub_body c u b i x = match kind_of_term x with
+      | Const (c',u') when eq_constant c c' -> 
+	let subst = 
+	  Array.fold_left2 (fun subst l l' -> Univ.LMap.add l l' subst)
+	    Univ.LMap.empty (Instance.to_array u) (Instance.to_array u')
+	in 
+	  Vars.subst_univs_level_constr subst b
+      | _ -> map_constr_with_binders ((+) 1) (fun i x -> sub_body c u b i x) i x in
     let fix_body (c,cb) t =
       match cb.const_body with
       | Undef _ -> assert false
       | Def b ->
           let b = Mod_subst.force_constr b in
-          let b_ty = Typeops.type_of_constant_type env cb.const_type in
-          let t = sub c 1 (Vars.lift 1 t) in
-          mkLetIn (cname c, b, b_ty, t)
+	  let poly = cb.const_polymorphic in
+	    if not poly then
+              let b_ty = Typeops.type_of_constant_type env cb.const_type in
+              let t = sub c 1 (Vars.lift 1 t) in
+		mkLetIn (cname c, b, b_ty, t)
+	    else 
+	      let univs = Future.force cb.const_universes in
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
       | OpaqueDef b -> 
           let b = Opaqueproof.force_proof b in
-          let b_ty = Typeops.type_of_constant_type env cb.const_type in
-          let t = sub c 1 (Vars.lift 1 t) in
-          mkApp (mkLambda (cname c, b_ty, t), [|b|]) in
-    List.fold_right fix_body cbl t
+	  let poly = cb.const_polymorphic in
+	    if not poly then
+              let b_ty = Typeops.type_of_constant_type env cb.const_type in
+              let t = sub c 1 (Vars.lift 1 t) in
+		mkApp (mkLambda (cname c, b_ty, t), [|b|]) 
+	    else
+	      let univs = Future.force cb.const_universes in
+		sub_body c (Univ.UContext.instance univs) b 1 (Vars.lift 1 t)
+    in
+      List.fold_right fix_body cbl t
   in
   (* CAVEAT: we assure a proper order *)
   Declareops.fold_side_effects handle_sideff body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index c149bb1acc..ea3ab16a51 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -109,7 +109,7 @@ sig
   val equal : t -> t -> bool
   (** Equality function on formal universes *)
 
-  (* val hash : t -> int *)
+  val hash : t -> int
   (** Hash function *)
 
   val make : Level.t -> t