- Fix abstract forgetting about new constraints.

library/universes.ml

@@ -144,8 +144,7 @@ let constr_of_global gr =
     else c
 
 let unsafe_constr_of_global gr =
-  let c, ctx = unsafe_global_instance (Global.env ()) gr in
-    c
+  unsafe_global_instance (Global.env ()) gr
 
 let constr_of_global_univ (gr,u) =
   match gr with

library/universes.mli

@@ -145,9 +145,9 @@ val normalize_universe_subst : universe_subst ref ->
 val constr_of_global : Globnames.global_reference -> constr
 
 (** [unsafe_constr_of_global gr] turns [gr] into a constr, works on polymorphic
-    reference by building a "dummy" universe instance that is not recorded 
+    references by taking the original universe instance that is not recorded 
     anywhere. The constraints are forgotten as well. DO NOT USE in new code. *)
-val unsafe_constr_of_global : Globnames.global_reference -> constr
+val unsafe_constr_of_global : Globnames.global_reference -> constr in_universe_context
 
 val type_of_global : Globnames.global_reference -> types in_universe_context_set
 

plugins/funind/functional_principles_types.ml

@@ -645,7 +645,7 @@ let build_case_scheme fa =
 (*     Constrintern.global_reference  id *)
 (*   in  *)
   let funs =  (fun (_,f,_) ->
-		 try Universes.unsafe_constr_of_global (Nametab.global f)
+		 try fst (Universes.unsafe_constr_of_global (Nametab.global f))
 		 with Not_found ->
 		   Errors.error ("Cannot find "^ Libnames.string_of_reference f)) fa in
   let first_fun,u = destConst  funs in

plugins/funind/recdef.ml

@@ -75,7 +75,8 @@ let type_of_const t =
     Const sp -> Typeops.type_of_constant (Global.env()) sp
     |_ -> assert false
 
-let constr_of_global = Universes.unsafe_constr_of_global
+let constr_of_global x = 
+  fst (Universes.unsafe_constr_of_global x)
 
 let constant sl s = constr_of_global (find_reference sl s)
 

tactics/tactics.ml

@@ -3763,8 +3763,8 @@ let abstract_subproof id tac =
   (** 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 *)
-  (* FIXME: lem might have generated new constraints... not taken into account *)
-  let lem = Universes.unsafe_constr_of_global (ConstRef cst) in
+  let lem, ctx = Universes.unsafe_constr_of_global (ConstRef cst) in
+  let evd = Evd.merge_context_set Evd.univ_flexible evd (Univ.ContextSet.of_context ctx) 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