- 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

5 files changed, 79 insertions, 17 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
diff --git a/library/universes.ml b/library/universes.ml
index 99c8b39f95..b37970b38a 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -55,6 +55,9 @@ let fresh_instance_from ctx =
   let constraints = instantiate_univ_context subst ctx in
     (inst, subst), (ctx', constraints)
 
+let unsafe_instance_from ctx =
+  (Univ.UContext.instance ctx, ctx)
+
 (** Fresh universe polymorphic construction *)
 
 let fresh_constant_instance env c =
@@ -78,7 +81,29 @@ let fresh_constructor_instance env (ind,i) =
 	(((ind,i),inst), ctx)
     else (((ind,i),Instance.empty), ContextSet.empty)
 
+let unsafe_constant_instance env c =
+  let cb = lookup_constant c env in
+    if cb.Declarations.const_polymorphic then
+      let inst, ctx = unsafe_instance_from (Future.force cb.Declarations.const_universes) in
+	((c, inst), ctx)
+    else ((c,Instance.empty), UContext.empty)
+
+let unsafe_inductive_instance env ind = 
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+    if mib.Declarations.mind_polymorphic then
+      let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
+	((ind,inst), ctx)
+    else ((ind,Instance.empty), UContext.empty)
+
+let unsafe_constructor_instance env (ind,i) = 
+  let mib, mip = Inductive.lookup_mind_specif env ind in
+    if mib.Declarations.mind_polymorphic then
+      let inst, ctx = unsafe_instance_from mib.Declarations.mind_universes in
+	(((ind,i),inst), ctx)
+    else (((ind,i),Instance.empty), UContext.empty)
+
 open Globnames
+
 let fresh_global_instance env gr =
   match gr with
   | VarRef id -> mkVar id, ContextSet.empty
@@ -92,6 +117,19 @@ let fresh_global_instance env gr =
      let c, ctx = fresh_inductive_instance env sp in
        mkIndU c, ctx
 
+let unsafe_global_instance env gr =
+  match gr with
+  | VarRef id -> mkVar id, UContext.empty
+  | ConstRef sp -> 
+     let c, ctx = unsafe_constant_instance env sp in
+       mkConstU c, ctx
+  | ConstructRef sp ->
+     let c, ctx = unsafe_constructor_instance env sp in
+       mkConstructU c, ctx
+  | IndRef sp -> 
+     let c, ctx = unsafe_inductive_instance env sp in
+       mkIndU c, ctx
+
 let constr_of_global gr =
   let c, ctx = fresh_global_instance (Global.env ()) gr in
     if not (Univ.ContextSet.is_empty ctx) then
@@ -106,7 +144,7 @@ let constr_of_global gr =
     else c
 
 let unsafe_constr_of_global gr =
-  let c, ctx = fresh_global_instance (Global.env ()) gr in
+  let c, ctx = unsafe_global_instance (Global.env ()) gr in
     c
 
 let constr_of_global_univ (gr,u) =
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 75504ee072..764f06a0fd 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3007,7 +3007,7 @@ let compute_scheme_signature scheme names_info ind_type_guess =
    different. *)
 let compute_elim_signature (evd,(elimc,elimt),ind_type_guess) names_info =
   let scheme = compute_elim_sig ~elimc:elimc elimt in
-  compute_scheme_signature scheme names_info ind_type_guess, scheme
+    evd, (compute_scheme_signature scheme names_info ind_type_guess, scheme)
 
 let guess_elim isrec hyp0 gl =
   let tmptyp0 =	pf_get_hyp_typ gl hyp0 in
@@ -3049,7 +3049,7 @@ let find_induction_type isrec elim hyp0 gl =
 	let evd, (elimc,elimt),_ = guess_elim isrec hyp0 gl in
 	let scheme = compute_elim_sig ~elimc elimt in
 	(* We drop the scheme waiting to know if it is dependent *)
-	project gl, scheme, ElimOver (isrec,hyp0)
+	evd, scheme, ElimOver (isrec,hyp0)
     | Some e ->
 	let evd, (elimc,elimt),ind_guess = given_elim hyp0 e gl in
 	let scheme = compute_elim_sig ~elimc elimt in
@@ -3080,8 +3080,8 @@ let get_eliminator elim gl = match elim with
       Proofview.Goal.sigma gl, (* bugged, should be computed *) true, elim, indsign
   | ElimOver (isrec,id) ->
       let evd, (elimc,elimt),_ as elims = Tacmach.New.of_old (guess_elim isrec id) gl in
-      evd, isrec, ({elimindex = None; elimbody = elimc}, elimt),
-      fst (compute_elim_signature elims id)
+      let _, (l, _) = compute_elim_signature elims id in
+      evd, isrec, ({elimindex = None; elimbody = elimc}, elimt), l
 
 (* Instantiate all meta variables of elimclause using lid, some elts
    of lid are parameters (first ones), the other are
@@ -3269,7 +3269,7 @@ let induction_with_atomization_of_ind_arg isrec with_evars elim names (hyp0,lbin
    parameters and arguments are given (mandatory too). *)
 let induction_without_atomization isrec with_evars elim names lid =
   Proofview.Goal.enter begin fun gl ->
-  let (indsign,scheme as elim_info) = Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) gl in
+  let sigma, (indsign,scheme as elim_info) = Tacmach.New.of_old (find_elim_signature isrec elim (List.hd lid)) gl in
   let awaited_nargs =
     scheme.nparams + scheme.nargs
     + (if scheme.farg_in_concl then 1 else 0)
@@ -3278,7 +3278,9 @@ let induction_without_atomization isrec with_evars elim names lid =
   let nlid = List.length lid in
   if not (Int.equal nlid awaited_nargs)
   then Proofview.tclZERO (Errors.UserError ("", str"Not the right number of induction arguments."))
-  else induction_from_context_l with_evars elim_info lid names
+  else 
+    Proofview.tclTHEN (Proofview.V82.tclEVARS sigma)
+      (induction_from_context_l with_evars elim_info lid names)
   end
 
 let has_selected_occurrences = function
@@ -3760,7 +3762,9 @@ let abstract_subproof id tac =
   let decl = (cd, IsProof Lemma) in
   (** ppedrot: seems legit to have abstracted subproofs as local*)
   let cst = Declare.declare_constant ~internal:Declare.KernelSilent ~local:true id decl in
-  let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in
+  (* let evd, lem = Evd.fresh_global (Global.env ()) evd (ConstRef cst) in *)
+  (* FIXME: lem might have generated new constraints... not taken into account *)
+  let lem = Universes.unsafe_constr_of_global (ConstRef cst) in
   let open Declareops in
   let eff = Safe_typing.sideff_of_con (Global.safe_env ()) cst in
   let effs = cons_side_effects eff no_seff in
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 450b6ee51f..bb702f79f7 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1838,7 +1838,8 @@ let check_vernac_supports_locality c l =
     | VernacSetOpacity _ | VernacSetStrategy _
     | VernacSetOption _ | VernacUnsetOption _
     | VernacDeclareReduction _
-    | VernacExtend _ ) -> ()
+    | VernacExtend _ 
+    | VernacInductive _) -> ()
   | Some _, _ -> Errors.error "This command does not support Locality"
 
 (* Vernaculars that take a polymorphism flag *)