- 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.

1 files changed, 2 insertions, 0 deletions

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)