Merge branch 'v8.5'

17 files changed, 206 insertions, 59 deletions

diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index 4da901e53..6074acea4 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -487,9 +487,7 @@ let ppist ist =
 (* Vernac-level debugging commands                                    *)
 
 let in_current_context f c =
-  let (evmap,sign) =
-    try Pfedit.get_current_goal_context ()
-    with e when Logic.catchable_exception e -> (Evd.empty, Global.env()) in
+  let (evmap,sign) = Pfedit.get_current_context () in
   f (fst (Constrintern.interp_constr sign evmap c))(*FIXME*)
 
 (* We expand the result of preprocessing to be independent of camlp4
diff --git a/kernel/byterun/coq_interp.c b/kernel/byterun/coq_interp.c
index bf383a33a..df5fdce75 100644
--- a/kernel/byterun/coq_interp.c
+++ b/kernel/byterun/coq_interp.c
@@ -903,10 +903,12 @@ value coq_interprete
 	  Alloc_small(block, 2, ATOM_PROJ_TAG);
 	  Field(block, 0) = Field(coq_global_data, *pc);
 	  Field(block, 1) = accu;
-	  /* Create accumulator */
-	  Alloc_small(accu, 2, Accu_tag);
-	  Code_val(accu) = accumulate;
-	  Field(accu, 1) = block;
+          accu = block;
+          /* Create accumulator */
+          Alloc_small(block, 2, Accu_tag);
+          Code_val(block) = accumulate;
+          Field(block, 1) = accu;
+          accu = block;
 	} else {
 	    accu = Field(accu, *pc++);
 	}
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml
index cd8ce7e87..cb39df8ab 100644
--- a/ltac/rewrite.ml
+++ b/ltac/rewrite.ml
@@ -1825,10 +1825,10 @@ let declare_projection n instance_id r =
   let poly = Global.is_polymorphic r in
   let env = Global.env () in
   let sigma = Evd.from_env env in
-  let evd,c = Evd.fresh_global env sigma r in
+  let sigma,c = Evd.fresh_global env sigma r in
   let ty = Retyping.get_type_of env sigma c in
   let term = proper_projection c ty in
-  let typ = Typing.unsafe_type_of env sigma term in
+  let sigma, typ = Typing.type_of env sigma term in
   let ctx, typ = decompose_prod_assum typ in
   let typ =
     let n =
@@ -1857,9 +1857,7 @@ let declare_projection n instance_id r =
     ignore(Declare.declare_constant n 
 	   (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition))
 
-let build_morphism_signature m =
-  let env = Global.env () in
-  let sigma = Evd.from_env env in
+let build_morphism_signature env sigma m =
   let m,ctx = Constrintern.interp_constr env sigma m in
   let sigma = Evd.from_ctx ctx in
   let t = Typing.unsafe_type_of env sigma m in
@@ -1884,8 +1882,10 @@ let build_morphism_signature m =
   in
   let morph = e_app_poly env evd PropGlobal.proper_type [| t; sig_; m |] in
   let evd = solve_constraints env !evd in
-  let m = Evarutil.nf_evar evd morph in
-    Pretyping.check_evars env Evd.empty evd m; m
+  let evd = Evd.nf_constraints evd in
+  let m = Evarutil.nf_evars_universes evd morph in
+  Pretyping.check_evars env Evd.empty evd m;
+  Evd.evar_universe_context evd, m
 
 let default_morphism sign m =
   let env = Global.env () in
@@ -1922,12 +1922,13 @@ let add_morphism_infer glob m n =
   init_setoid ();
   let poly = Flags.is_universe_polymorphism () in
   let instance_id = add_suffix n "_Proper" in
-  let instance = build_morphism_signature m in
-  let evd = Evd.from_env (Global.env ()) in
+  let env = Global.env () in
+  let evd = Evd.from_env env in
+  let uctx, instance = build_morphism_signature env evd m in
     if Lib.is_modtype () then
       let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
 				(Entries.ParameterEntry 
-				 (None,poly,(instance,Univ.UContext.empty),None), 
+				 (None,poly,(instance,Evd.evar_context_universe_context uctx),None), 
 				 Decl_kinds.IsAssumption Decl_kinds.Logical)
       in
 	add_instance (Typeclasses.new_instance 
@@ -1950,7 +1951,7 @@ let add_morphism_infer glob m n =
       let hook = Lemmas.mk_hook hook in
 	Flags.silently
 	  (fun () ->
-	    Lemmas.start_proof instance_id kind evd instance hook;
+	    Lemmas.start_proof instance_id kind (Evd.from_ctx uctx) instance hook;
 	    ignore (Pfedit.by (Tacinterp.interp tac))) ()
 
 let add_morphism glob binders m s n =
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 4072109c4..e40621965 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -989,7 +989,10 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_typ (Mod_subst.force_constr c)
+	      | Some pb -> mk_typ pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
@@ -998,7 +1001,10 @@ let extract_constant env kn cb =
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (Mod_subst.force_constr c)
+	  | Def c ->
+	     (match cb.const_proj with
+	      | None -> mk_def (Mod_subst.force_constr c)
+	      | Some pb -> mk_def pb.proj_body)
 	  | OpaqueDef c ->
 	    add_opaque r;
 	    if access_opaque () then
diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 6a03e2d61..88b13abf9 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -212,9 +212,11 @@ let find t k =
 	res
 
 let memo cache f =
-  let tbl = lazy (open_in cache) in
-    fun x ->
-      let tbl = Lazy.force tbl in
+  let tbl = lazy (try Some (open_in cache) with _ -> None) in
+  fun x ->
+  match Lazy.force tbl with
+  | None -> f x
+  | Some tbl ->
 	try
 	  find tbl x
 	with
diff --git a/printing/printer.ml b/printing/printer.ml
index a43ccff46..cc8da4097 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -28,10 +28,7 @@ let delayed_emacs_cmd s =
   if !Flags.print_emacs then s () else str ""
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    let env = Global.env () in
-    (Evd.from_env env, env)
+  Pfedit.get_current_context ()
 
 (**********************************************************************)
 (** Terms                                                             *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 45af036fb..2863384b5 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -71,23 +71,34 @@ let get_nth_V82_goal i =
   with Failure _ -> raise NoSuchGoal
     
 let get_goal_context_gen i =
-  try
-let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
-(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
-  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+  let { it=goal ; sigma=sigma; } =  get_nth_V82_goal i in
+  (sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
 
 let get_goal_context i =
   try get_goal_context_gen i
-  with NoSuchGoal -> Errors.error "No such goal."
+  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+     | NoSuchGoal -> Errors.error "No such goal."
 
 let get_current_goal_context () =
   try get_goal_context_gen 1
-  with NoSuchGoal ->
+  with Proof_global.NoCurrentProof -> Errors.error "No focused proof."
+     | NoSuchGoal -> 
     (* spiwack: returning empty evar_map, since if there is no goal, under focus,
         there is no accessible evar either *)
     let env = Global.env () in
     (Evd.from_env env, env)
 
+let get_current_context () =
+  try get_goal_context_gen 1
+  with Proof_global.NoCurrentProof ->
+    let env = Global.env () in
+    (Evd.from_env env, env)
+     | NoSuchGoal ->
+        (* No more focused goals ? *)
+        let p = get_pftreestate () in
+        let evd = Proof.in_proof p (fun x -> x) in
+        (evd, Global.env ())
+
 let current_proof_statement () =
   match Proof_global.V82.get_current_initial_conclusions () with
     | (id,([concl],strength)) -> id,strength,concl
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index cd8992015..cfab8bd63 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -93,6 +93,14 @@ val get_goal_context : int -> Evd.evar_map * env
 
 val get_current_goal_context : unit -> Evd.evar_map * env
 
+(** [get_current_context ()] returns the context of the
+  current focused goal. If there is no focused goal but there
+  is a proof in progress, it returns the corresponding evar_map.
+  If there is no pending proof then it returns the current global
+  environment and empty evar_map. *)
+
+val get_current_context : unit -> Evd.evar_map * env
+
 (** [current_proof_statement] *)
 
 val current_proof_statement :
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index 0ca4d6020..a7b381ad6 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -124,7 +124,7 @@ module Make(T : Task) = struct
                  "-async-proofs-worker-priority";
                    Flags.string_of_priority !Flags.async_proofs_worker_priority]
         | ("-ideslave"|"-emacs"|"-emacs-U"|"-batch")::tl -> set_slave_opt tl
-        | ("-async-proofs" |"-toploop" |"-vi2vo"
+        | ("-async-proofs" |"-toploop" |"-vio2vo"
           |"-load-vernac-source" |"-l" |"-load-vernac-source-verbose" |"-lv"
           |"-compile" |"-compile-verbose"
           |"-async-proofs-worker-priority" |"-worker-id") :: _ :: tl ->
diff --git a/stm/lemmas.ml b/stm/lemmas.ml
index afbc407d8..0a63a3a0f 100644
--- a/stm/lemmas.ml
+++ b/stm/lemmas.ml
@@ -520,13 +520,5 @@ let save_proof ?proof = function
 (* Miscellaneous *)
 
 let get_current_context () =
-  try Pfedit.get_current_goal_context ()
-  with e when Logic.catchable_exception e ->
-    try (* No more focused goals ? *)
-      let p = Pfedit.get_pftreestate () in
-      let evd = Proof.in_proof p (fun x -> x) in
-      (evd, Global.env ())
-    with Proof_global.NoCurrentProof ->
-      let env = Global.env () in
-      (Evd.from_env env, env)
+  Pfedit.get_current_context ()
            
diff --git a/stm/lemmas.mli b/stm/lemmas.mli
index 9120787d1..f751598f0 100644
--- a/stm/lemmas.mli
+++ b/stm/lemmas.mli
@@ -65,4 +65,3 @@ val save_proof : ?proof:Proof_global.closed_proof -> Vernacexpr.proof_end -> uni
    and the current global env *)
 
 val get_current_context : unit -> Evd.evar_map * Environ.env
-
diff --git a/tactics/hints.ml b/tactics/hints.ml
index b543b564c..6f8da00d8 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -707,10 +707,43 @@ let make_apply_entry env sigma (eapply,hnf,verbose) pri poly ?(name=PathAny) (c,
    c is a constr
    cty is the type of constr *)
 
+let pr_hint_term env sigma ctx = function
+  | IsGlobRef gr -> pr_global gr
+  | IsConstr (c, ctx) ->
+     let sigma = Evd.merge_context_set Evd.univ_flexible sigma ctx in
+     pr_constr_env env sigma c
+
+(** We need an object to record the side-effect of registering
+  global universes associated with a hint. *)
+let cache_context_set (_,c) =
+  Global.push_context_set false c
+
+let input_context_set : Univ.ContextSet.t -> Libobject.obj =
+  let open Libobject in
+    declare_object
+    { (default_object "Global universe context") with
+      cache_function = cache_context_set;
+      load_function = (fun _ -> cache_context_set);
+      discharge_function = (fun (_,a) -> Some a);
+      classify_function = (fun a -> Keep a) }
+
 let fresh_global_or_constr env sigma poly cr =
-  match cr with
-  | IsGlobRef gr -> Universes.fresh_global_instance env gr
-  | IsConstr (c, ctx) -> (c, ctx)
+  let isgr, (c, ctx) =
+    match cr with
+    | IsGlobRef gr ->
+       true, Universes.fresh_global_instance env gr
+    | IsConstr (c, ctx) -> false, (c, ctx)
+  in
+    if poly then (c, ctx)
+    else if Univ.ContextSet.is_empty ctx then (c, ctx)
+    else begin
+      if isgr then
+        Feedback.msg_warning (str"Using polymorphic hint " ++
+		     pr_hint_term env sigma ctx cr ++ str" monomorphically" ++
+		     str" use Polymorphic Hint to use it polymorphically.");
+      Lib.add_anonymous_leaf (input_context_set ctx);
+      (c, Univ.ContextSet.empty)
+    end
 
 let make_resolves env sigma flags pri poly ?name cr =
   let c, ctx = fresh_global_or_constr env sigma poly cr in
@@ -1077,7 +1110,7 @@ let prepare_hint check (poly,local) env init (sigma,c) =
     let diff = Univ.ContextSet.diff (Evd.universe_context_set sigma) (Evd.universe_context_set init) in
     if poly then IsConstr (c', diff)
     else if local then IsConstr (c', diff)
-    else (Global.push_context_set false diff;
+    else (Lib.add_anonymous_leaf (input_context_set diff);
 	  IsConstr (c', Univ.ContextSet.empty))
 
 let interp_hints poly =
@@ -1152,18 +1185,24 @@ let expand_constructor_hints env sigma lems =
     match kind_of_term lem with
     | Ind (ind,u) ->
 	List.init (nconstructors ind) 
-	  (fun i -> IsConstr (mkConstructU ((ind,i+1),u), 
-			      Univ.ContextSet.empty))
+		  (fun i ->
+		   let ctx = Univ.ContextSet.diff (Evd.universe_context_set evd)
+						  (Evd.universe_context_set sigma) in
+		   not (Univ.ContextSet.is_empty ctx),
+		   IsConstr (mkConstructU ((ind,i+1),u),ctx))
     | _ ->
-	[prepare_hint false (false,true) env sigma (evd,lem)]) lems
-
+       [match prepare_hint false (false,true) env sigma (evd,lem) with
+	| IsConstr (c, ctx) ->
+	   not (Univ.ContextSet.is_empty ctx), IsConstr (c, ctx)
+	| IsGlobRef _ -> assert false (* Impossible return value *) ]) lems
 (* builds a hint database from a constr signature *)
 (* typically used with (lid, ltyp) = pf_hyps_types <some goal> *)
 
 let add_hint_lemmas env sigma eapply lems hint_db =
   let lems = expand_constructor_hints env sigma lems in
   let hintlist' =
-    List.map_append (make_resolves env sigma (eapply,true,false) None false) lems in
+    List.map_append (fun (poly, lem) ->
+		     make_resolves env sigma (eapply,true,false) None poly lem) lems in
   Hint_db.add_list env sigma hintlist' hint_db
 
 let make_local_hint_db env sigma ts eapply lems =
@@ -1182,12 +1221,6 @@ let make_local_hint_db env sigma ts eapply lems =
   add_hint_lemmas env sigma eapply lems
     (Hint_db.add_list env sigma hintlist (Hint_db.empty ts false))
 
-let make_local_hint_db = 
-  if Flags.profile then
-    let key = Profile.declare_profile "make_local_hint_db" in
-      Profile.profile4 key make_local_hint_db
-  else make_local_hint_db
-
 let make_local_hint_db env sigma ?ts eapply lems =
   make_local_hint_db env sigma ts eapply lems
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a2431f6ef..75273e4b7 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1377,6 +1377,8 @@ let general_elim with_evars clear_flag (c, lbindc) elim =
   let t = try snd (reduce_to_quantified_ind env sigma ct) with UserError _ -> ct in
   let elimtac = elimination_clause_scheme with_evars in
   let indclause  = make_clenv_binding env sigma (c, t) lbindc in
+  let sigma = meta_merge sigma (clear_metas indclause.evd) in
+  Proofview.Unsafe.tclEVARS sigma <*>
   Tacticals.New.tclTHEN
     (general_elim_clause_gen elimtac indclause elim)
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c)
diff --git a/test-suite/bugs/closed/4498.v b/test-suite/bugs/closed/4498.v
new file mode 100644
index 000000000..ccdb2dddd
--- /dev/null
+++ b/test-suite/bugs/closed/4498.v
@@ -0,0 +1,24 @@
+Require Export Coq.Unicode.Utf8.
+Require Export Coq.Classes.Morphisms.
+Require Export Coq.Relations.Relation_Definitions.
+
+Set Universe Polymorphism.
+
+Reserved Notation "a ~> b" (at level 90, right associativity).
+
+Class Category := {
+  ob            : Type;
+  uhom          := Type : Type;
+  hom           : ob → ob → uhom where "a ~> b" := (hom a b);
+  compose       : ∀ {A B C}, (B ~> C) → (A ~> B) → (A ~> C);
+  equiv         : ∀ {A B}, relation (A ~> B);
+  is_equiv      : ∀ {A B}, @Equivalence (A ~> B) equiv;
+  comp_respects : ∀ {A B C},
+      Proper (@equiv B C ==> @equiv A B ==> @equiv A C) (@compose A B C);
+}.
+
+Require Export Coq.Setoids.Setoid.
+
+Add Parametric Morphism `{C : Category} {A B C} : (@compose _ A B C) with
+  signature equiv ==> equiv ==> equiv as compose_mor.
+Proof. apply comp_respects. Qed.
\ No newline at end of file
diff --git a/test-suite/bugs/closed/4628.v b/test-suite/bugs/closed/4628.v
new file mode 100644
index 000000000..7d4a15d68
--- /dev/null
+++ b/test-suite/bugs/closed/4628.v
@@ -0,0 +1,46 @@
+Module first.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End first.
+
+Module firstbest.
+  Polymorphic Record BAR (A:Type) :=
+  { foo: A->Prop; bar: forall (x y: A), foo x -> foo y}.
+
+Section A.
+Context {A:Type}.
+
+Set Printing Universes.
+
+Polymorphic Hint Resolve bar.
+Goal forall (P:BAR A) x y, foo _ P x -> foo _ P y.
+intros.
+eauto.
+Qed.
+End A.
+End firstbest.
+
+Module second.
+Axiom foo: Set.
+Axiom foo': Set.
+
+Polymorphic Record BAR (A:Type) :=
+  { bar: foo' -> foo}.
+Set Printing Universes.
+
+Lemma baz@{i}: forall (P:BAR@{Set} nat), foo' -> foo.
+  eauto using bar.
+Qed.
+End second.
diff --git a/test-suite/bugs/closed/4710.v b/test-suite/bugs/closed/4710.v
new file mode 100644
index 000000000..fdc850109
--- /dev/null
+++ b/test-suite/bugs/closed/4710.v
@@ -0,0 +1,12 @@
+Set Primitive Projections.
+Record Foo' := Foo { foo : nat }.
+Extraction foo.
+Record Foo2 (a : nat) := Foo2c { foo2p : nat; foo2b : bool }.
+Extraction Language Ocaml.
+Extraction foo2p.
+
+Definition bla (x : Foo2 0) := foo2p _ x.
+Extraction bla.
+
+Definition bla' (a : nat) (x : Foo2 a) := foo2b _ x.
+Extraction bla'.
diff --git a/test-suite/bugs/closed/4746.v b/test-suite/bugs/closed/4746.v
new file mode 100644
index 000000000..d64cc6fe6
--- /dev/null
+++ b/test-suite/bugs/closed/4746.v
@@ -0,0 +1,14 @@
+Variables P Q : nat -> Prop.
+Variable f : nat -> nat.
+
+Goal forall (x:nat), (forall y, P y -> forall z, Q z -> y=f z -> False) -> False.
+Proof.
+intros.
+ecase H with (3:=eq_refl).
+Abort.
+
+Goal forall (x:nat), (forall y, y=x -> False) -> False.
+Proof.
+intros.
+unshelve ecase H with (1:=eq_refl).
+Qed.