- Fix eq_constr_universes restricted to Sorts.equal

- Fix passing of universe contexts through definitions/proofs, abstract is ok now, even
  in presence of polymorphism
- Correctly mark unresolvable the evars made by the Simple abstraction.

4 files changed, 31 insertions, 18 deletions

diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index eeb5770253..077057f3cc 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -119,13 +119,12 @@ open Decl_kinds
 let next = let n = ref 0 in fun () -> incr n; !n
 
 let build_constant_by_tactic id sign ?(goal_kind = Global, false, Proof Theorem) typ tac =
-  let substref = ref Univ.LMap.empty in (** FIXME: Something wrong here with subst *)
   start_proof id goal_kind sign typ (fun _ -> ());
   try
     let status = by tac in
-    let _,(const,_,_) = cook_proof () in
+    let _,(const,univs,_) = cook_proof () in
     delete_current_proof ();
-    const, status, !substref
+    const, status, univs
   with reraise ->
     let reraise = Errors.push reraise in
     delete_current_proof ();
@@ -135,11 +134,11 @@ let build_by_tactic env ?(poly=false) typ tac =
   let id = Id.of_string ("temporary_proof"^string_of_int (next())) in
   let sign = val_of_named_context (named_context env) in
   let gk = Global, poly, Proof Theorem in
-  let ce, status, subst = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
+  let ce, status, univs = build_constant_by_tactic id sign ~goal_kind:gk typ tac in
   let ce = Term_typing.handle_side_effects env ce in
   let cb, se = Future.force ce.const_entry_body in
   assert(Declareops.side_effects_is_empty se);
-  cb, status, subst
+  cb, status, fst univs
 
 (**********************************************************************)
 (* Support for resolution of evars in tactic interpretation, including
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index e3df619f82..615866c6ae 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -149,7 +149,9 @@ val instantiate_nth_evar_com : int -> Constrexpr.constr_expr -> unit
 
 val build_constant_by_tactic :
   Id.t -> named_context_val -> ?goal_kind:goal_kind ->
-    types Univ.in_universe_context_set -> unit Proofview.tactic -> Entries.definition_entry * bool * Universes.universe_opt_subst
+    types Univ.in_universe_context_set -> unit Proofview.tactic -> 
+  Entries.definition_entry * bool * Universes.universe_opt_subst Univ.in_universe_context
+
 val build_by_tactic : env -> ?poly:polymorphic -> 
   types Univ.in_universe_context_set -> unit Proofview.tactic -> 
   constr Univ.in_universe_context_set * bool * Universes.universe_opt_subst
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 12700851aa..e49a57af39 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -264,16 +264,12 @@ let get_open_goals () =
     (List.map (fun (l1,l2) -> List.length l1 + List.length l2) gll) +
     List.length shelf
 
-let nf_body nf b =
-  let aux ((c, ctx), t) = ((nf c, ctx), t) in
-    Future.chain ~pure:true b aux
-
 let close_proof ?feedback_id ~now fpl =
   let { pid; section_vars; strength; proof; terminator } = cur_pstate () in
   let poly = pi2 strength (* Polymorphic *) in
   let initial_goals = Proof.initial_goals proof in
   let fpl, univs = Future.split2 fpl in
-  let (subst, univs as univsubst), nf = 
+  let univsubst, make_body =
     if poly || now then
       let usubst, uctx = Future.force univs in
       let ctx, subst = 
@@ -286,29 +282,43 @@ let close_proof ?feedback_id ~now fpl =
       let subst = 
 	Univ.LMap.union usubst (Univ.LMap.map (fun v -> Some (Univ.Universe.make v)) subst)
       in
-	(subst, Univ.ContextSet.to_context ctx), nf
+      let univsubst = (subst, Univ.ContextSet.to_context ctx) in
+      let make_body p _c t _octx =
+	let (c, ctx), eff = Future.force p in
+	let body = nf c and typ = nf t in
+	let used_univs = 
+	  Univ.LSet.union (Universes.universes_of_constr body)
+	    (Universes.universes_of_constr typ)
+	in
+	let ctx = Universes.restrict_universe_context ctx used_univs in
+	let p = Future.from_val ((body, Univ.ContextSet.empty),eff) in
+	let univs = Univ.ContextSet.to_context ctx in
+	  univs, p, typ
+      in univsubst, make_body
     else
       let ctx = 
 	List.fold_left (fun acc (c, (t, octx)) -> 
 	  Univ.ContextSet.union octx acc)
 	  Univ.ContextSet.empty initial_goals
       in
-	(Univ.LMap.empty, Univ.ContextSet.to_context ctx), (fun x -> x)
+      let univs = Univ.ContextSet.to_context ctx in
+      let univsubst = (Univ.LMap.empty, univs) in
+	univsubst, (fun p c t octx -> univs, p, t)
   in
   let entries =
-    Future.map2 (fun p (c, (t, octx)) -> { Entries.
-      const_entry_body = nf_body nf p;
+    Future.map2 (fun p (c, (t, octx)) -> 
+      let univs, body, typ = make_body p c t octx in
+      { Entries.
+      const_entry_body = body;
       const_entry_secctx = section_vars;
       const_entry_feedback = feedback_id;
-      const_entry_type  = Some (nf t);
+      const_entry_type  = Some typ;
       const_entry_inline_code = false;
       const_entry_opaque = true;
       const_entry_universes = univs;
       const_entry_polymorphic = poly;
       const_entry_proj = None})
     fpl initial_goals in
-  if now then
-    List.iter (fun x ->ignore(Future.force x.Entries.const_entry_body)) entries;
   { id = pid; entries = entries; persistence = strength; universes = univsubst },
   Ephemeron.get terminator
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 291da4a983..83a703a3a9 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -838,6 +838,8 @@ struct
   let new_evar (evd, evs) env typ =
     let src = (Loc.ghost, Evar_kinds.GoalEvar) in
     let (evd, ev) = Evarutil.new_evar evd env ~src typ in
+    let evd = Typeclasses.mark_unresolvables 
+      ~filter:(fun ev' _ -> Evar.equal (fst (Term.destEvar ev)) ev') evd in
     let (evk, _) = Term.destEvar ev in
     let h = (evd, build_goal evk :: evs) in
     (h, ev)