Merge branch 'v8.5'

22 files changed, 190 insertions, 99 deletions

diff --git a/checker/inductive.ml b/checker/inductive.ml
index 43a32ea24..6f9b5f204 100644
--- a/checker/inductive.ml
+++ b/checker/inductive.ml
@@ -59,16 +59,6 @@ let inductive_instance mib =
     UContext.instance mib.mind_universes
   else Instance.empty
 
-let inductive_context mib =
-  if mib.mind_polymorphic then 
-    instantiate_univ_context mib.mind_universes 
-  else UContext.empty
-
-let instantiate_inductive_constraints mib u =
-  if mib.mind_polymorphic then
-    subst_instance_constraints u (UContext.constraints mib.mind_universes)
-  else Constraint.empty
-
 (************************************************************************)
 
 (* Build the substitution that replaces Rels by the appropriate *)
@@ -190,8 +180,6 @@ let rec make_subst env =
   in
   make Univ.LMap.empty
 
-exception SingletonInductiveBecomesProp of Id.t
-
 let instantiate_universes env ctx ar argsorts =
   let args = Array.to_list argsorts in
   let subst = make_subst env (ctx,ar.template_param_levels,args) in
@@ -208,11 +196,7 @@ let instantiate_universes env ctx ar argsorts =
 
 (* Type of an inductive type *)
 
-let is_prop_sort = function
-  | Prop Null -> true
-  | _ -> false
-
-let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
+let type_of_inductive_gen env ((mib,mip),u) paramtyps =
   match mip.mind_arity with
   | RegularArity a ->
     if not mib.mind_polymorphic then a.mind_user_arity
@@ -220,25 +204,7 @@ let type_of_inductive_gen ?(polyprop=true) env ((mib,mip),u) paramtyps =
   | TemplateArity ar ->
     let ctx = List.rev mip.mind_arity_ctxt in
     let ctx,s = instantiate_universes env ctx ar paramtyps in
-      (* The Ocaml extraction cannot handle (yet?) "Prop-polymorphism", i.e.
-         the situation where a non-Prop singleton inductive becomes Prop
-         when applied to Prop params *)
-      if not polyprop && not (Univ.is_type0m_univ ar.template_level) && is_prop_sort s
-      then raise (SingletonInductiveBecomesProp mip.mind_typename);
-      mkArity (List.rev ctx,s)
-
-let type_of_inductive env pind = 
-  type_of_inductive_gen env pind [||]
-
-let constrained_type_of_inductive env ((mib,mip),u as pind) =
-  let ty = type_of_inductive_gen env pind [||] in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
-
-let constrained_type_of_inductive_knowing_parameters env ((mib,mip),u as pind) args =
-  let ty = type_of_inductive_gen env pind args in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
+    mkArity (List.rev ctx,s)
 
 let type_of_inductive_knowing_parameters env mip args = 
   type_of_inductive_gen env mip args
@@ -275,16 +241,6 @@ let type_of_constructor_gen (cstr,u) (mib,mip as mspec) =
 let type_of_constructor cstru mspec = 
   type_of_constructor_gen cstru mspec
 
-let type_of_constructor_in_ctx cstr (mib,mip as mspec) =
-  let u = Univ.UContext.instance mib.mind_universes in
-  let c = type_of_constructor_gen (cstr, u) mspec in
-    (c, mib.mind_universes)
-
-let constrained_type_of_constructor (cstr,u as cstru) (mib,mip as ind) =
-  let ty = type_of_constructor_gen cstru ind in
-  let cst = instantiate_inductive_constraints mib u in
-    (ty, cst)
-
 let arities_of_specif (kn,u) (mib,mip) =
   let specif = mip.mind_nf_lc in
   Array.map (constructor_instantiate kn u mib) specif
diff --git a/doc/refman/Extraction.tex b/doc/refman/Extraction.tex
index 9da23b54e..01dbcfb1c 100644
--- a/doc/refman/Extraction.tex
+++ b/doc/refman/Extraction.tex
@@ -448,7 +448,7 @@ let dp x y f = Pair ((Obj.magic f () x), (Obj.magic f () y))
     happens when there is a quantification over types inside the type
     of a constructor; for example:
 \begin{verbatim}
-Inductive anything : Set := dummy : forall A:Set, A -> anything.
+Inductive anything : Type := dummy : forall A:Set, A -> anything.
 \end{verbatim}
 
 which corresponds to the definition of an ML dynamic type.
diff --git a/ide/coq.ml b/ide/coq.ml
index 11621078d..6d44ca59e 100644
--- a/ide/coq.ml
+++ b/ide/coq.ml
@@ -227,7 +227,7 @@ type coqtop = {
   (* non quoted command-line arguments of coqtop *)
   mutable sup_args : string list;
   (* called whenever coqtop dies *)
-  mutable reset_handler : reset_kind -> unit task;
+  mutable reset_handler : unit task;
   (* called whenever coqtop sends a feedback message *)
   mutable feedback_handler : Feedback.feedback -> unit;
   (* actual coqtop process and its status *)
@@ -421,6 +421,7 @@ let mkready coqtop =
   fun () -> coqtop.status <- Ready; Void
 
 let rec respawn_coqtop ?(why=Unexpected) coqtop =
+  if why = Unexpected then warning "Coqtop died badly. Resetting.";
   clear_handle coqtop.handle;
   ignore_error (fun () ->
      coqtop.handle <-
@@ -432,7 +433,7 @@ let rec respawn_coqtop ?(why=Unexpected) coqtop =
      If not, there isn't much we can do ... *)
   assert (coqtop.handle.alive = true);
   coqtop.status <- New;
-  ignore (coqtop.reset_handler why coqtop.handle (mkready coqtop))
+  ignore (coqtop.reset_handler coqtop.handle (mkready coqtop))
 
 let spawn_coqtop sup_args =
   bind_self_as (fun this -> {
@@ -440,7 +441,7 @@ let spawn_coqtop sup_args =
                (fun () -> respawn_coqtop (this ()))
                (fun msg -> (this ()).feedback_handler msg);
     sup_args = sup_args;
-    reset_handler = (fun _ _ k -> k ());
+    reset_handler = (fun _ k -> k ());
     feedback_handler = (fun _ -> ());
     status = New;
   })
diff --git a/ide/coq.mli b/ide/coq.mli
index 7cef6a4d0..8a1fa3ed1 100644
--- a/ide/coq.mli
+++ b/ide/coq.mli
@@ -60,7 +60,7 @@ val is_computing : coqtop -> bool
 val spawn_coqtop : string list -> coqtop
 (** Create a coqtop process with some command-line arguments. *)
 
-val set_reset_handler : coqtop -> (reset_kind -> unit task) -> unit
+val set_reset_handler : coqtop -> unit task -> unit
 (** Register a handler called when a coqtop dies (badly or on purpose) *)
 
 val set_feedback_handler : coqtop -> (Feedback.feedback -> unit) -> unit
diff --git a/ide/coqOps.ml b/ide/coqOps.ml
index c912adcf1..f0e767cba 100644
--- a/ide/coqOps.ml
+++ b/ide/coqOps.ml
@@ -136,7 +136,7 @@ object
   method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
-  method handle_reset_initial : Coq.reset_kind -> unit task
+  method handle_reset_initial : unit task
   method raw_coq_query : string -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
@@ -844,10 +844,8 @@ object(self)
     in
     loop l
 
-  method handle_reset_initial why =
+  method handle_reset_initial =
     let action () =
-      if why = Coq.Unexpected then warning "Coqtop died badly. Resetting."
-      else
       (* clear the stack *)
       if Doc.focused document then Doc.unfocus document;
       while not (Doc.is_empty document) do
diff --git a/ide/coqOps.mli b/ide/coqOps.mli
index 4a37a1fa5..332c18f2f 100644
--- a/ide/coqOps.mli
+++ b/ide/coqOps.mli
@@ -15,7 +15,7 @@ object
   method tactic_wizard : string list -> unit task
   method process_next_phrase : unit task
   method process_until_end_or_error : unit task
-  method handle_reset_initial : Coq.reset_kind -> unit task
+  method handle_reset_initial : unit task
   method raw_coq_query : string -> unit task
   method show_goals : unit task
   method backtrack_last_phrase : unit task
diff --git a/library/lib.ml b/library/lib.ml
index f8bb6bac5..f580050db 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -417,7 +417,7 @@ let add_section_variable id impl poly ctx =
   match !sectab with
     | [] -> () (* because (Co-)Fixpoint temporarily uses local vars *)
     | (vars,repl,abs)::sl ->
-       check_same_poly poly vars;
+       List.iter (fun tab -> check_same_poly poly (pi1 tab)) !sectab;
        sectab := (Variable (id,impl,poly,ctx)::vars,repl,abs)::sl
 
 let add_section_context ctx =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index e40621965..0153348de 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -36,7 +36,7 @@ let current_fixpoints = ref ([] : constant list)
 let none = Evd.empty
 
 (* NB: In OCaml, [type_of] and [get_of] might raise
-   [SingletonInductiveBecomeProp]. this exception will be catched
+   [SingletonInductiveBecomeProp]. This exception will be caught
    in late wrappers around the exported functions of this file,
    in order to display the location of the issue. *)
 
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 95b4967fa..e742f7b80 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -1516,13 +1516,13 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
   let functional_id =  add_suffix function_name "_F" in
   let term_id = add_suffix function_name "_terminate" in
   let functional_ref = declare_fun functional_id (IsDefinition Decl_kinds.Definition) ~ctx:(snd (Evd.universe_context evm)) res in
+  (* Refresh the global universes, now including those of _F *)
+  let evm = Evd.from_env (Global.env ()) in
   let env_with_pre_rec_args = push_rel_context(List.map (function (x,t) -> LocalAssum (x,t)) pre_rec_args) env in
-  let relation =
-    fst (*FIXME*)(interp_constr
-      env_with_pre_rec_args
-      (Evd.from_env env_with_pre_rec_args)
-      r)
+  let relation, evuctx =
+    interp_constr env_with_pre_rec_args evm r
   in
+  let evm = Evd.from_ctx evuctx in
   let tcc_lemma_name = add_suffix function_name "_tcc" in
   let tcc_lemma_constr = ref None in
   (* let _ = Pp.msgnl (str "relation := " ++ Printer.pr_lconstr_env env_with_pre_rec_args relation) in *)
diff --git a/pretyping/coercion.ml b/pretyping/coercion.ml
index 5c7adf1aa..c168e070f 100644
--- a/pretyping/coercion.ml
+++ b/pretyping/coercion.ml
@@ -513,7 +513,7 @@ let inh_conv_coerce_to_gen resolve_tc rigidonly loc env evd cj t =
 	      error_actual_type_loc loc env best_failed_evd cj t e
 	    else 
       	      inh_conv_coerce_to_fail loc env evd' rigidonly (Some cj.uj_val) cj.uj_type t
-	  with NoCoercionNoUnifier (best_failed_evd,e) ->
+	  with NoCoercionNoUnifier (_evd,_error) ->
 	    error_actual_type_loc loc env best_failed_evd cj t e
   in
   let val' = match val' with Some v -> v | None -> assert(false) in
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index 39f581082..a2e8fac05 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -487,9 +487,11 @@ let save_proof ?proof = function
             let ctx = Evd.evar_context_universe_context (fst universes) in
             Admitted(id, k, (const_entry_secctx, pi2 k, (typ, ctx), None), universes)
         | None ->
+            let pftree = Pfedit.get_pftreestate () in
             let id, k, typ = Pfedit.current_proof_statement () in
+            let universes = Proof.initial_euctx pftree in
             (* This will warn if the proof is complete *)
-            let pproofs, universes =
+            let pproofs, _univs =
               Proof_global.return_proof ~allow_partial:true () in
             let sec_vars =
               match  Pfedit.get_used_variables(), pproofs with
@@ -501,7 +503,8 @@ let save_proof ?proof = function
                   Some (Environ.keep_hyps env (Idset.union ids_typ ids_def))
               | _ -> None in
 	    let names = Pfedit.get_universe_binders () in
-            let binders, ctx = Evd.universe_context ?names (Evd.from_ctx universes) in
+            let evd = Evd.from_ctx universes in
+            let binders, ctx = Evd.universe_context ?names evd in
             Admitted(id,k,(sec_vars, pi2 k, (typ, ctx), None),
 		     (universes, Some binders))
       in
diff --git a/tactics/auto.ml b/tactics/auto.ml
index e57b48e9e..6c1f38d48 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -94,7 +94,7 @@ let connect_hint_clenv poly (c, _, ctx) clenv gl =
       let evd = Evd.merge_context_set Evd.univ_flexible evd ctx in
       { clenv with evd = evd ; env = Proofview.Goal.env gl }, c
   in clenv, c
-		     
+
 let unify_resolve poly flags ((c : raw_hint), clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
   let clenv, c = connect_hint_clenv poly c clenv gl in
@@ -109,21 +109,11 @@ let unify_resolve_gen poly = function
   | Some flags -> unify_resolve poly flags
 
 let exact poly (c,clenv) =
-  let (c, _, _) = c in
-  let ctx, c' = 
-    if poly then
-      let evd', subst = Evd.refresh_undefined_universes clenv.evd in
-      let ctx = Evd.evar_universe_context evd' in
-	ctx, subst_univs_level_constr subst c 
-    else 
-      let ctx = Evd.evar_universe_context clenv.evd in
-	ctx, c
-  in
-  Proofview.Goal.s_enter { s_enter = begin fun gl ->
-    let sigma = Proofview.Goal.sigma gl in
-    let sigma = Sigma.to_evar_map sigma in
-    let sigma = Evd.merge_universe_context sigma ctx in
-    Sigma.Unsafe.of_pair (exact_check c', sigma)
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let clenv', c = connect_hint_clenv poly c clenv gl in
+    Tacticals.New.tclTHEN
+    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+    (exact_check c)
   end }
 
 (* Util *)
diff --git a/tactics/auto.mli b/tactics/auto.mli
index 0fd95aead..1608a0ea6 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -22,8 +22,8 @@ val default_search_depth : int ref
 val auto_flags_of_state : transparent_state -> Unification.unify_flags
 
 val connect_hint_clenv : polymorphic -> raw_hint -> clausenv ->
-			 ([ `NF ], 'r) Proofview.Goal.t -> clausenv * constr
-						
+  ('a, 'r) Proofview.Goal.t -> clausenv * constr
+
 (** Try unification with the precompiled clause, then use registered Apply *)
 val unify_resolve : polymorphic -> Unification.unify_flags -> (raw_hint * clausenv) -> unit Proofview.tactic
 
diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 2cae9b794..93c201bf1 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -108,7 +108,7 @@ open Auto
 (***************************************************************************)
 
 let priority l = List.map snd (List.filter (fun (pr,_) -> Int.equal pr 0) l)
-			  
+
 let unify_e_resolve poly flags (c,clenv) =
   Proofview.Goal.nf_enter { enter = begin fun gl ->
       let clenv', c = connect_hint_clenv poly c clenv gl in
@@ -128,11 +128,12 @@ let hintmap_of hdc concl =
    (* FIXME: should be (Hint_db.map_eauto hdc concl db) *)
 
 let e_exact poly flags (c,clenv) =
-  let (c, _, _) = c in
-  let clenv', subst = 
-    if poly then Clenv.refresh_undefined_univs clenv 
-    else clenv, Univ.empty_level_subst
-  in e_give_exact (* ~flags *) (Vars.subst_univs_level_constr subst c)
+  Proofview.Goal.enter { enter = begin fun gl ->
+    let clenv', c = connect_hint_clenv poly c clenv gl in
+    Tacticals.New.tclTHEN
+    (Proofview.Unsafe.tclEVARUNIVCONTEXT (Evd.evar_universe_context clenv'.evd))
+    (e_give_exact c)
+  end }
 
 let rec e_trivial_fail_db db_list local_db =
   let next = Proofview.Goal.nf_enter { enter = begin fun gl ->
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 95bf1babe..952719129 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1096,10 +1096,12 @@ exception Found of constr * types
 
 let prepare_hint check (poly,local) env init (sigma,c) =
   let sigma = Typeclasses.resolve_typeclasses ~fail:false env sigma in
-  (* We re-abstract over uninstantiated evars.
+  (* We re-abstract over uninstantiated evars and universes.
      It is actually a bit stupid to generalize over evars since the first
      thing make_resolves will do is to re-instantiate the products *)
-  let c = drop_extra_implicit_args (Evarutil.nf_evar sigma c) in
+  let sigma, subst = Evd.nf_univ_variables sigma in
+  let c = Vars.subst_univs_constr subst (Evarutil.nf_evar sigma c) in
+  let c = drop_extra_implicit_args c in
   let vars = ref (collect_vars c) in
   let subst = ref [] in
   let rec find_next_evar c = match kind_of_term c with
diff --git a/test-suite/bugs/closed/4450.v b/test-suite/bugs/closed/4450.v
new file mode 100644
index 000000000..ecebaba81
--- /dev/null
+++ b/test-suite/bugs/closed/4450.v
@@ -0,0 +1,58 @@
+Polymorphic Axiom inhabited@{u} : Type@{u} -> Prop.
+
+Polymorphic Axiom unit@{u} : Type@{u}.
+Polymorphic Axiom tt@{u} : inhabited unit@{u}.
+
+Polymorphic Hint Resolve tt : the_lemmas.
+Set Printing All.
+Set Printing Universes.
+Goal inhabited unit.
+Proof.
+  eauto with the_lemmas.
+Qed.
+
+Universe u.
+Axiom f : Type@{u} -> Prop.
+Lemma fapp (X : Type) : f X -> False.
+Admitted.
+Polymorphic Axiom funi@{i} : f unit@{i}.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto using (fapp unit funi). (* The two fapp's have different universes *)
+Qed.
+
+Hint Resolve (fapp unit funi) : mylems.
+
+Goal (forall U, f U) -> (*(f unit -> False) ->  *)False /\ False.
+  eauto with mylems. (* Forces the two fapps at the same level *)
+Qed.
+
+Goal (forall U, f U) -> (f unit -> False) -> False /\ False.
+  eauto. (* Forces the two fapps at the same level *)
+Qed.
+
+Polymorphic Definition MyType@{i} := Type@{i}.
+Universes l m n.
+Constraint l < m.
+Polymorphic Axiom maketype@{i} : MyType@{i}.
+
+Goal MyType@{l}.
+Proof.
+  Fail solve [ eauto using maketype@{m} ].
+  eauto using maketype.
+  Undo.
+  eauto using maketype@{n}.
+Qed.
+
+Axiom foo : forall (A : Type), list A.
+Polymorphic Axiom foop@{i} : forall (A : Type@{i}), list A.
+
+Universe x y.
+Goal list Type@{x}.
+Proof.
+  eauto using (foo Type). (* Refreshes the term *)
+  Undo.
+  eauto using foo. Show Universes.
+  Undo.
+  eauto using foop. Show Proof. Show Universes.
+Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4725.v b/test-suite/bugs/closed/4725.v
new file mode 100644
index 000000000..fd5e0fb60
--- /dev/null
+++ b/test-suite/bugs/closed/4725.v
@@ -0,0 +1,38 @@
+Require Import EquivDec Equivalence List Program.
+Require Import Relation_Definitions.
+Import ListNotations.
+Generalizable All Variables.
+
+Fixpoint removeV `{eqDecV : @EqDec V eqV equivV}`(x : V) (l : list V) : list V
+:=
+  match l with
+  | nil => nil
+  | y::tl => if (equiv_dec x y) then removeV x tl else y::(removeV x tl)
+  end.
+
+Lemma remove_le {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV :
+@EqDec V eqV equivV} (xs : list V) (x : V) :
+  length (removeV x xs) < length (x :: xs).
+  Proof. Admitted.
+
+(* Function version *)
+Set Printing Universes.
+
+Require Import Recdef.
+
+Function nubV {V:Type}{eqV:relation V}{equivV:@Equivalence V eqV}{eqDecV :
+@EqDec V eqV equivV} (l : list V) { measure length l} :=
+    match l with
+      | nil => nil
+      | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs)
+    end.
+Proof. intros. apply remove_le. Qed.
+
+(* Program version *)
+
+Program Fixpoint nubV `{eqDecV : @EqDec V eqV equivV} (l : list V)
+        {  measure (@length V l) lt } :=
+    match l with
+      | nil => nil
+      | x::xs => x :: @nubV V eqV equivV eqDecV (removeV x xs) _
+    end.
diff --git a/test-suite/bugs/closed/4782.v b/test-suite/bugs/closed/4782.v
index ed4443786..dbd71035d 100644
--- a/test-suite/bugs/closed/4782.v
+++ b/test-suite/bugs/closed/4782.v
@@ -7,3 +7,18 @@ Inductive p : Prop := consp : forall (e : r) (x : type e), cond e x -> p.
 Goal p.
 Fail apply consp with (fun _ : bool => mk_r unit (fun x => True)) nil.
  
+(* A simplification of an example from coquelicot, which was failing
+   at some time after a fix #4782 was committed. *)
+
+Record T := { dom : Type }.
+Definition pairT A B := {| dom := (dom A * dom B)%type |}.
+Class C (A:Type).
+Parameter B:T.
+Instance c (A:T) : C (dom A).
+Instance cn : C (dom B).
+Parameter F : forall A:T, C (dom A) -> forall x:dom A, x=x -> A = A.
+Set Typeclasses Debug.
+Goal forall (A:T) (x:dom A), pairT A A = pairT A A.
+intros.
+apply (F _ _)  with (x,x).
+  
diff --git a/test-suite/bugs/closed/4816.v b/test-suite/bugs/closed/4816.v
index 86597c88f..00a523842 100644
--- a/test-suite/bugs/closed/4816.v
+++ b/test-suite/bugs/closed/4816.v
@@ -15,3 +15,15 @@ Section Foo.
     Fail Constraint X <= Z.
   End Bar.
 End Foo.
+
+Require Coq.Classes.RelationClasses.
+
+Class PreOrder (A : Type) (r : A -> A -> Type) : Type :=
+{ refl : forall x, r x x }.
+
+Section qux.
+  Polymorphic Universes A.
+  Section bar.
+    Fail Context {A : Type@{A}} {rA : A -> A -> Prop} {PO : PreOrder A rA}.
+  End bar.
+End qux.
diff --git a/test-suite/bugs/closed/4818.v b/test-suite/bugs/closed/4818.v
new file mode 100644
index 000000000..904abb228
--- /dev/null
+++ b/test-suite/bugs/closed/4818.v
@@ -0,0 +1,24 @@
+(* -*- mode: coq; coq-prog-args: ("-emacs" "-R" "." "Prob" "-top" "Product") -*- *)
+(* File reduced by coq-bug-finder from original input, then from 391 lines to 77 lines, then from 857 lines to 119 lines, then from 1584 lines to 126 lines, then from 362 lines to 135 lines, then from 149 lines to 135 lines *)
+(* coqc version 8.5pl1 (June 2016) compiled on Jun 9 2016 17:27:17 with OCaml 4.02.3
+   coqtop version 8.5pl1 (June 2016) *)
+Set Universe Polymorphism.
+
+Inductive GCov (I : Type) : Type := | Foo : I -> GCov I.
+
+Section Product.
+
+Variables S IS : Type.
+Variable locS : IS -> True.
+
+Goal GCov (IS * S) -> GCov IS.
+intros X0. induction X0; intros.
+destruct i.
+specialize (locS i).
+clear -locS. 
+destruct locS. Show Universes.
+Admitted.
+
+(*
+Anomaly: Universe Product.5189 undefined. Please report.
+*)
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 1fda5b9f7..28fa8a171 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -934,7 +934,6 @@ let build_wellfounded (recname,pl,n,bl,arityc,body) poly r measure notation =
   let binders = letbinders @ [arg] in
   let binders_env = push_rel_context binders_rel env in
   let rel, _ = interp_constr_evars_impls env evdref r in
-  let () = check_evars_are_solved env !evdref (Evd.empty,!evdref)  in
   let relty = Typing.unsafe_type_of env !evdref rel in
   let relargty =
     let error () =
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 4d8d537f2..ccc8e2ffe 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -23,10 +23,6 @@ open Util
 let declare_fix_ref = ref (fun ?opaque _ _ _ _ _ _ -> assert false)
 let declare_definition_ref = ref (fun _ _ _ _ _ -> assert false)
 
-let trace s =
-  if !Flags.debug then Feedback.msg_debug s
-  else ()
-
 let succfix (depth, fixrels) =
   (succ depth, List.map succ fixrels)
 
@@ -895,8 +891,6 @@ let rec solve_obligation prg num tac =
   let terminator guard hook = Proof_global.make_terminator (obligation_terminator prg.prg_name num guard hook) in
   let hook ctx = Lemmas.mk_hook (obligation_hook prg obl num auto ctx) in
   let () = Lemmas.start_proof_univs ~sign:prg.prg_sign obl.obl_name kind evd obl.obl_type ~terminator hook in
-  let () = trace (str "Started obligation " ++ int user_num ++ str "  proof: " ++
-            Printer.pr_constr_env (Global.env ()) Evd.empty obl.obl_type) in
   let _ = Pfedit.by !default_tactic in
   Option.iter (fun tac -> Pfedit.set_end_tac tac) tac