From 55e62174683f293c8f966d8bd486fcb511f66221 Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Wed, 11 Dec 2013 17:19:01 +0000
Subject: - 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
---
 kernel/term_typing.ml | 33 ++++++++++++++++++++++++++-------
 kernel/univ.mli       |  2 +-
 2 files changed, 27 insertions(+), 8 deletions(-)

(limited to 'kernel')

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
-- 
cgit v1.2.3