Merge branch 'v8.5'

30 files changed, 214 insertions, 79 deletions

diff --git a/checker/check.mllib b/checker/check.mllib
index 3725989e8..900cfe0c8 100644
--- a/checker/check.mllib
+++ b/checker/check.mllib
@@ -33,7 +33,7 @@ CStack
 Util
 Ppstyle
 Errors
-Ephemeron
+CEphemeron
 Future
 CUnix
 
diff --git a/dev/printers.mllib b/dev/printers.mllib
index bb627f590..21868203f 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -48,7 +48,7 @@ Rtree
 Heap
 Genarg
 Stateid
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
 Monad
diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex
index edf986392..f5a1bf3b2 100644
--- a/doc/refman/RefMan-tac.tex
+++ b/doc/refman/RefMan-tac.tex
@@ -3648,9 +3648,6 @@ The {\hintdef} is one of the following expressions:
   the number of subgoals generated by {\tt simple apply {\term}}.
 %{\tt auto} actually uses a slightly modified variant of {\tt simple apply} with use_metas_eagerly_in_conv_on_closed_terms set to false
 
-  The cost of that hint is the number of subgoals generated by that
-  tactic.
-
   % Is it really needed?
   %% In case the inferred type of \term\ does not start with a product
   %% the tactic added in the hint list is {\tt exact {\term}}. In case
@@ -3848,7 +3845,25 @@ is to set the cut expression to $c | e$, the initial cut expression
 being \texttt{emp}.
 
 
+\item \texttt{Mode} {\tt (+ | -)}$^*$ {\qualid}
+\label{HintMode}
+\comindex{Hint Mode}
+
+This sets an optional mode of use of the identifier {\qualid}.  When
+proof-search faces a goal that ends in an application of {\qualid} to
+arguments {\tt \term$_1$ \mbox{\dots} \term$_n$}, the mode tells if the
+hints associated to qualid can be applied or not. A mode specification 
+is a list of $n$ {\tt +} or {\tt -} items that specify if an argument is
+to be treated as an input {\tt +} or an output {\tt -} of the
+identifier. For a mode to match a list of arguments, input terms \emph{must
+not} contain existential variables, while outputs can be any term.
+Multiple modes can be declared for a single identifier, in that case 
+only one mode needs to match the arguments for the hints to be applied.
 
+{\tt Hint Mode} is especially useful for typeclasses, when one does not
+want to support default instances and avoid ambiguity in
+general. Setting a parameter of a class as an input forces proof-search
+to be driven by that index of the class.
 
 \end{itemize}
 
@@ -3856,25 +3871,6 @@ being \texttt{emp}.
 pattern-matching on hypotheses using \texttt{match goal with} inside
 the tactic.
 
-\begin{Variants}
-\item {\tt Hint \hintdef}
-
-  No database name is given: the hint is registered in the {\tt core}
-    database.
-
-\item {\tt Hint Local {\hintdef} : \ident$_1$ \mbox{\dots} \ident$_n$}
-
-  This is used to declare hints that must not be exported to the other
-  modules that require and import the current module. Inside a
-  section, the option {\tt Local} is useless since hints do not
-  survive anyway to the closure of sections.
-
-\item {\tt Hint Local \hintdef}
-
-  Idem for the {\tt core} database.
-
-\end{Variants}
-
 % There are shortcuts that allow to define several goal at once:
 
 % \begin{itemize}
diff --git a/interp/notation.ml b/interp/notation.ml
index 04918bf7d..ab0dcbeb7 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -314,7 +314,9 @@ let declare_prim_token_interpreter sc interp (patl,uninterp,b) =
     patl
 
 let mkNumeral n = Numeral n
-let mkString s = String s
+let mkString = function
+| None -> None
+| Some s -> if Unicode.is_utf8 s then Some (String s) else None
 
 let delay dir int loc x = (dir, (fun () -> int loc x))
 
@@ -326,7 +328,7 @@ let declare_numeral_interpreter sc dir interp (patl,uninterp,inpat) =
 let declare_string_interpreter sc dir interp (patl,uninterp,inpat) =
   declare_prim_token_interpreter sc
     (fun cont loc -> function String s -> delay dir interp loc s | p -> cont loc p)
-    (patl, (fun r -> Option.map mkString (uninterp r)), inpat)
+    (patl, (fun r -> mkString (uninterp r)), inpat)
 
 let check_required_module loc sc (sp,d) =
   try let _ = Nametab.global_of_path sp in ()
diff --git a/kernel/csymtable.ml b/kernel/csymtable.ml
index 9d58f6615..047da682a 100644
--- a/kernel/csymtable.ml
+++ b/kernel/csymtable.ml
@@ -130,8 +130,8 @@ let key rk =
   match !rk with
   | None -> raise NotEvaluated
   | Some k ->
-      try Ephemeron.get k
-      with Ephemeron.InvalidKey -> raise NotEvaluated
+      try CEphemeron.get k
+      with CEphemeron.InvalidKey -> raise NotEvaluated
 
 (************************)
 (* traduction des patch *)
@@ -170,7 +170,7 @@ let rec slot_for_getglobal env kn =
 	 | BCconstant -> set_global (val_of_constant kn)
     in
 (*Pp.msgnl(str"value stored at: "++int pos);*)
-    rk := Some (Ephemeron.create pos);
+    rk := Some (CEphemeron.create pos);
     pos
 
 and slot_for_fv env fv =
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 3ecfcca64..d07ca2103 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -104,7 +104,7 @@ type side_eff =
   | SEscheme of (inductive * constant * Declarations.constant_body * seff_env) list * string
 
 type side_effect = {
-  from_env : Declarations.structure_body Ephemeron.key;
+  from_env : Declarations.structure_body CEphemeron.key;
   eff      : side_eff;
 }
 
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 229508ea3..551632962 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -794,7 +794,15 @@ let rec subterm_specif renv stack t =
     | Proj (p, c) -> 
       let subt = subterm_specif renv stack c in
 	(match subt with
-	| Subterm (s, wf) -> Subterm (Strict, wf)
+	| Subterm (s, wf) ->
+	   (* We take the subterm specs of the constructor of the record *)
+	   let wf_args = (dest_subterms wf).(0) in
+	   (* We extract the tree of the projected argument *)
+	   let kn = Projection.constant p in
+	   let cb = lookup_constant kn renv.env in
+	   let pb = Option.get cb.const_proj in
+	   let n = pb.proj_arg in
+	   Subterm (Strict, List.nth wf_args n)
 	| Dead_code -> Dead_code
 	| Not_subterm -> Not_subterm)
 
diff --git a/kernel/pre_env.ml b/kernel/pre_env.ml
index 99d99e694..0e56e76aa 100644
--- a/kernel/pre_env.ml
+++ b/kernel/pre_env.ml
@@ -25,7 +25,7 @@ open Context.Named.Declaration
 (* The key attached to each constant is used by the VM to retrieve previous *)
 (* evaluations of the constant. It is essentially an index in the symbols table *)
 (* used by the VM. *)
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 (** Linking information for the native compiler. *)
 
@@ -50,17 +50,17 @@ type stratification = {
 }
 
 type val_kind =
-    | VKvalue of (values * Id.Set.t) Ephemeron.key
+    | VKvalue of (values * Id.Set.t) CEphemeron.key
     | VKnone
 
 type lazy_val = val_kind ref
 
 let force_lazy_val vk = match !vk with
 | VKnone -> None
-| VKvalue v -> try Some (Ephemeron.get v) with Ephemeron.InvalidKey -> None
+| VKvalue v -> try Some (CEphemeron.get v) with CEphemeron.InvalidKey -> None
 
 let dummy_lazy_val () = ref VKnone
-let build_lazy_val vk key = vk := VKvalue (Ephemeron.create key)
+let build_lazy_val vk key = vk := VKvalue (CEphemeron.create key)
 
 type named_vals = (Id.t * lazy_val) list
 
diff --git a/kernel/pre_env.mli b/kernel/pre_env.mli
index f626aa0d3..353c46112 100644
--- a/kernel/pre_env.mli
+++ b/kernel/pre_env.mli
@@ -17,7 +17,7 @@ type link_info =
   | LinkedInteractive of string
   | NotLinked
 
-type key = int Ephemeron.key option ref 
+type key = int CEphemeron.key option ref 
 
 type constant_key = constant_body * (link_info ref * key)
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 8a402322f..ce05190b6 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -225,11 +225,11 @@ let side_effects_of_private_constants x = Term_typing.uniq_seff (List.rev x)
 
 let private_con_of_con env c =
   let cbo = Environ.lookup_constant c env.env in
-  { Entries.from_env = Ephemeron.create env.revstruct;
+  { Entries.from_env = CEphemeron.create env.revstruct;
     Entries.eff      = Entries.SEsubproof (c,cbo,get_opaque_body env.env cbo) }
 
 let private_con_of_scheme ~kind env cl =
-  { Entries.from_env = Ephemeron.create env.revstruct;
+  { Entries.from_env = CEphemeron.create env.revstruct;
     Entries.eff      = Entries.SEscheme(
       List.map (fun (i,c) ->
         let cbo = Environ.lookup_constant c env.env in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2a3ac957f..3839135a8 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -125,14 +125,14 @@ let check_signatures curmb sl =
     | None -> None, None
     | Some curmb ->
         try
-          let mb = Ephemeron.get mb in
+          let mb = CEphemeron.get mb in
           match sl with
           | None -> sl, None
           | Some n ->
               if List.length mb >= how_many && CList.skipn how_many mb == curmb
               then Some (n + how_many), Some mb
               else None, None
-        with Ephemeron.InvalidKey -> None, None in
+        with CEphemeron.InvalidKey -> None, None in
   let sl, _ = List.fold_left is_direct_ancestor (Some 0,Some curmb) sl in
   sl
 
diff --git a/lib/ephemeron.ml b/lib/cEphemeron.ml
index a38ea11e1..a38ea11e1 100644
--- a/lib/ephemeron.ml
+++ b/lib/cEphemeron.ml
diff --git a/lib/ephemeron.mli b/lib/cEphemeron.mli
index 1200e4e20..1200e4e20 100644
--- a/lib/ephemeron.mli
+++ b/lib/cEphemeron.mli
diff --git a/lib/future.ml b/lib/future.ml
index ff16286c4..9cdc1c20e 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -63,7 +63,7 @@ and 'a comp =
   | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
-  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
+  | Ongoing of string * (UUID.t * fix_exn * 'a comp ref) CEphemeron.key
   | Finished of 'a
 
 and 'a computation = 'a comput ref
@@ -71,13 +71,13 @@ and 'a computation = 'a comput ref
 let unnamed = "unnamed"
 
 let create ?(name=unnamed) ?(uuid=UUID.fresh ()) f x =
-  ref (Ongoing (name, Ephemeron.create (uuid, f, Pervasives.ref x)))
+  ref (Ongoing (name, CEphemeron.create (uuid, f, Pervasives.ref x)))
 let get x =
   match !x with
   | Finished v -> unnamed, UUID.invalid, id, ref (Val (v,None))
   | Ongoing (name, x) ->
-      try let uuid, fix, c = Ephemeron.get x in name, uuid, fix, c
-      with Ephemeron.InvalidKey ->
+      try let uuid, fix, c = CEphemeron.get x in name, uuid, fix, c
+      with CEphemeron.InvalidKey ->
         name, UUID.invalid, id, ref (Exn (NotHere name, Exninfo.null))
 
 type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn  ]
diff --git a/lib/lib.mllib b/lib/lib.mllib
index a9181c51c..2be435f6f 100644
--- a/lib/lib.mllib
+++ b/lib/lib.mllib
@@ -14,6 +14,6 @@ Rtree
 Heap
 Unionfind
 Genarg
-Ephemeron
+CEphemeron
 Future
 RemoteCounter
diff --git a/lib/unicode.ml b/lib/unicode.ml
index 05998bb80..938e8f1a9 100644
--- a/lib/unicode.ml
+++ b/lib/unicode.ml
@@ -173,6 +173,13 @@ let next_utf8 s i =
        (c land 0x3F) lsl 6 + (d land 0x3F)
   else err ()
 
+let is_utf8 s =
+  let rec check i =
+    let (off, _) = next_utf8 s i in
+    check (i + off)
+  in
+  try check 0 with End_of_input -> true | Invalid_argument _ -> false
+
 (* Check the well-formedness of an identifier *)
 
 let initial_refutation j n s =
diff --git a/lib/unicode.mli b/lib/unicode.mli
index 72d1f2950..b8a11e294 100644
--- a/lib/unicode.mli
+++ b/lib/unicode.mli
@@ -36,3 +36,6 @@ val is_basic_ascii : string -> bool
     translated to ["__Uxxxx_"] where {i xxxx} are four hexadecimal digits.
     @raise Unsupported if the input string contains unsupported UTF-8 characters. *)
 val ascii_of_ident : string -> string
+
+(** Validate an UTF-8 string *)
+val is_utf8 : string -> bool
diff --git a/library/library.ml b/library/library.ml
index c41e10608..8e2402dda 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -171,9 +171,8 @@ let register_loaded_library m =
     let prefix = Nativecode.mod_uid_of_dirpath libname ^ "." in
     let f = prefix ^ "cmo" in
     let f = Dynlink.adapt_filename f in
-    (* This will not produce errors or warnings if the native compiler was
-       not enabled *)
-    Nativelib.link_library ~prefix ~dirname ~basename:f
+    if not Coq_config.no_native_compiler then
+      Nativelib.link_library ~prefix ~dirname ~basename:f
   in
   let rec aux = function
     | [] -> link m; [libname]
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 7a933c04b..91a826c73 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -298,7 +298,7 @@ let build_functional_principle (evd:Evd.evar_map ref) interactive_proof old_prin
     (* 	  let dur1 = System.time_difference tim1 tim2 in *)
     (* 	  Pp.msgnl (str ("Time to compute proof: ") ++ str (string_of_float dur1)); *)
     (* 	end; *)
-    get_proof_clean true, Ephemeron.create hook
+    get_proof_clean true, CEphemeron.create hook
   end
 
 
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index aa47e2619..2449678a1 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -163,7 +163,7 @@ let save with_clean id const (locality,_,kind) hook =
 	(locality, ConstRef kn)
   in
   if with_clean then  Pfedit.delete_current_proof ();
-  Ephemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
+  CEphemeron.iter_opt hook (fun f -> Lemmas.call_hook fix_exn f l r);
   definition_message id
 
 
diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index 23f1da1ba..e5c756f56 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -47,7 +47,7 @@ val jmeq : unit -> Term.constr
 val jmeq_refl : unit -> Term.constr
 
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
-  unit Lemmas.declaration_hook Ephemeron.key -> unit
+  unit Lemmas.declaration_hook CEphemeron.key -> unit
 
 (* [get_proof_clean do_reduce] : returns the proof name, definition, kind and hook and
    abort the proof
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e68961da7..98fd658f2 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -488,7 +488,8 @@ let key_of env b flags f =
       Id.Pred.mem id (fst flags.modulo_delta) ->
     Some (IsKey (VarKey id))
   | Proj (p, c) when Projection.unfolded p
-      || Cpred.mem (Projection.constant p) (snd flags.modulo_delta) ->
+    || (is_transparent env (ConstKey (Projection.constant p)) &&
+       (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) ->
     Some (IsProj (p, c))
   | _ -> None
   
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 403a36141..d19dc5ba0 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -36,7 +36,7 @@ let find_proof_mode n =
     Errors.error (Format.sprintf "No proof mode named \"%s\"." n)
 
 let register_proof_mode ({name = n} as m) =
-  Hashtbl.add proof_modes n (Ephemeron.create m)
+  Hashtbl.add proof_modes n (CEphemeron.create m)
 
 (* initial mode: standard mode *)
 let standard = { name = "No" ; set = (fun ()->()) ; reset = (fun () -> ()) }
@@ -52,7 +52,7 @@ let _ =
     optname = "default proof mode" ;
     optkey = ["Default";"Proof";"Mode"] ;
     optread = begin fun () ->
-      (Ephemeron.default !default_proof_mode standard).name
+      (CEphemeron.default !default_proof_mode standard).name
     end;
     optwrite = begin fun n ->
       default_proof_mode := find_proof_mode n
@@ -83,12 +83,12 @@ type closed_proof = proof_object * proof_terminator
 
 type pstate = {
   pid : Id.t;
-  terminator : proof_terminator Ephemeron.key;
+  terminator : proof_terminator CEphemeron.key;
   endline_tactic : Tacexpr.raw_tactic_expr option;
   section_vars : Context.section_context option;
   proof : Proof.proof;
   strength : Decl_kinds.goal_kind;
-  mode : proof_mode Ephemeron.key;
+  mode : proof_mode CEphemeron.key;
   universe_binders: universe_binders option;
 }
 
@@ -106,11 +106,11 @@ let current_proof_mode = ref !default_proof_mode
 let update_proof_mode () =
   match !pstates with
   | { mode = m } :: _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := m;
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.set ())
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.set ())
   | _ ->
-      Ephemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
+      CEphemeron.iter_opt !current_proof_mode (fun x -> x.reset ());
       current_proof_mode := find_proof_mode "No"
 
 (* combinators for the current_proof lists *)
@@ -218,9 +218,9 @@ let set_proof_mode mn =
   set_proof_mode (find_proof_mode mn) (get_current_proof_name ())
 
 let activate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
+  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.set ())
 let disactivate_proof_mode mode =
-  Ephemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
+  CEphemeron.iter_opt (find_proof_mode mode) (fun x -> x.reset ())
 
 (** [start_proof sigma id str goals terminator] starts a proof of name
     [id] with goals [goals] (a list of pairs of environment and
@@ -233,7 +233,7 @@ let disactivate_proof_mode mode =
 let start_proof sigma id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.start sigma goals;
     endline_tactic = None;
     section_vars = None;
@@ -245,7 +245,7 @@ let start_proof sigma id ?pl str goals terminator =
 let start_dependent_proof id ?pl str goals terminator =
   let initial_state = {
     pid = id;
-    terminator = Ephemeron.create terminator;
+    terminator = CEphemeron.create terminator;
     proof = Proof.dependent_start goals;
     endline_tactic = None;
     section_vars = None;
@@ -384,7 +384,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now fpl =
   in
   { id = pid; entries = entries; persistence = strength;
     universes = (universes, binders) },
-  fun pr_ending -> Ephemeron.get terminator pr_ending
+  fun pr_ending -> CEphemeron.get terminator pr_ending
 
 type closed_proof_output = (Term.constr * Safe_typing.private_constants) list * Evd.evar_universe_context
 
@@ -432,11 +432,11 @@ let close_proof ~keep_body_ucst_separate fix_exn =
 
 (** Gets the current terminator without checking that the proof has
     been completed. Useful for the likes of [Admitted]. *)
-let get_terminator () = Ephemeron.get ( cur_pstate() ).terminator
+let get_terminator () = CEphemeron.get ( cur_pstate() ).terminator
 let set_terminator hook =
   match !pstates with
   | [] -> raise NoCurrentProof
-  | p :: ps -> pstates := { p with terminator = Ephemeron.create hook } :: ps
+  | p :: ps -> pstates := { p with terminator = CEphemeron.create hook } :: ps
 
 
 
diff --git a/stm/asyncTaskQueue.ml b/stm/asyncTaskQueue.ml
index bb312e3b1..1c6b542ab 100644
--- a/stm/asyncTaskQueue.ml
+++ b/stm/asyncTaskQueue.ml
@@ -312,7 +312,7 @@ module Make(T : Task) = struct
         let response = slave_respond request in
         report_status "Idle";
         marshal_response (Option.get !slave_oc) response;
-        Ephemeron.clear ()
+        CEphemeron.clear ()
       with
       | MarshalError s ->
         pr_err ("Fatal marshal error: " ^ s); flush_all (); exit 2
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 8eadd4aee..6c550e916 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -230,8 +230,8 @@ let rewrite_keyed_core_unif_flags = {
     (* This is set dynamically *)
 
   restrict_conv_on_strict_subterms = false;
-  modulo_betaiota = true;
-  (* Different from conv_closed *)
+  modulo_betaiota = false;
+
   modulo_eta = true;
 }
 
diff --git a/tactics/rewrite.ml b/tactics/rewrite.ml
index 8123bd755..953235463 100644
--- a/tactics/rewrite.ml
+++ b/tactics/rewrite.ml
@@ -484,11 +484,15 @@ let rec decompose_app_rel env evd t =
     let len = Array.length args in
     let fargs = Array.sub args 0 (Array.length args - 2) in
     let rel = mkApp (f, fargs) in
-    let ty = Retyping.get_type_of env evd rel in
-    let () = if not (Reduction.is_arity env ty) then error_no_relation () in
     rel, args.(len - 2), args.(len - 1)
   | _ -> error_no_relation ()
 
+let decompose_app_rel env evd t =
+  let (rel, t1, t2) = decompose_app_rel env evd t in
+  let ty = Retyping.get_type_of env evd rel in
+  let () = if not (Reduction.is_arity env ty) then error_no_relation () in
+  (rel, t1, t2)
+
 let decompose_applied_relation env sigma (c,l) =
   let open Context.Rel.Declaration in
   let ctype = Retyping.get_type_of env sigma c in
diff --git a/test-suite/bugs/closed/4596.v b/test-suite/bugs/closed/4596.v
new file mode 100644
index 000000000..592fdb658
--- /dev/null
+++ b/test-suite/bugs/closed/4596.v
@@ -0,0 +1,14 @@
+Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
+
+Definition T (x : bool) := x = true.
+
+Goal forall (S : Type) (b b0 : S -> nat -> bool) (str : S) (p : nat)
+  (s : forall n : nat, bool)
+  (s0 s1 : nat -> S -> S),
+  (forall (str0 : S) (n m : nat),
+  (if s m then T (b0 (s1 n str0) 0) else T (b (s1 n str0) 0)) -> T (b (s0 n str0) m) ->
+    T (b str0 m)) ->
+  T (b str p).
+Proof.
+intros ???????? H0.
+rewrite H0.
diff --git a/test-suite/success/auto.v b/test-suite/success/auto.v
index aaa7b3a51..5477c8331 100644
--- a/test-suite/success/auto.v
+++ b/test-suite/success/auto.v
@@ -45,3 +45,92 @@ Proof.
   eexists. Fail progress debug eauto with test2. 
   progress eauto with test.
 Qed.
+
+(** Patterns of Extern have a "matching" semantics.
+    It is not so for apply/exact hints *)
+
+Class B (A : Type).
+Class I. 
+Instance i : I.
+  
+Definition flip {A B C : Type} (f : A -> B -> C) := fun y x => f x y.
+Class D (f : nat -> nat -> nat).
+Definition ftest (x y : nat) := x + y.
+Definition flipD (f : nat -> nat -> nat) : D f -> D (flip f).
+  Admitted.
+Module Instnopat.
+  Local Instance: B nat.
+  (* pattern_of_constr -> B nat *)
+  (* exact hint *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+
+  Local Instance: D ftest.
+  Local Hint Resolve flipD | 0 : typeclass_instances.
+  (* pattern: D (flip _) *)
+  Fail Timeout 1 Check (_ : D _). (* loops applying flipD *)  
+  
+End Instnopat.
+
+Module InstnopatApply.
+  Local Instance: I -> B nat.
+  (* pattern_of_constr -> B nat *)
+  (* apply hint  *)
+  Check (_ : B nat).
+  (* map_eauto -> B_instance0 *)
+  (* NO Constr_matching.matches !!! *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    eauto with typeclass_instances.
+  Qed.
+End InstnopatApply.
+  
+Module InstPat.
+  Hint Extern 3 (B nat) => split : typeclass_instances.
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> true *)
+  Check (_ : B nat).
+  (* map_eauto -> Extern hint *)
+  (* Constr_matching.matches -> false:
+     Because an inductive in the pattern does not match an evar in the goal *)
+  Check (_ : B _).
+
+  Goal exists T, B T.
+    eexists.
+    (* map_existential -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail progress eauto with typeclass_instances.
+    (* map_eauto -> Extern hint *)
+    (* Constr_matching.matches -> false *)
+    Fail typeclasses eauto.
+  Abort.
+
+  Hint Extern 0 (D (flip _)) => apply flipD : typeclass_instances.
+  Module withftest.
+    Local Instance: D ftest.
+
+    Check (_ : D _).
+    (* D_instance_0 : D ftest *)
+    Check (_ : D (flip _)).
+    (* ... : D (flip ftest) *)
+  End withftest.
+  Module withoutftest.
+    Hint Extern 0 (D ftest) => split : typeclass_instances.
+    Check (_ : D _).
+    (* ? : D ?, _not_ looping *)
+    Check (_ : D (flip _)).
+    (* ? : D (flip ?), _not_ looping *)
+
+    Check (_ : D (flip ftest)).
+    (* flipD ftest {|  |} : D (flip ftest) *)
+  End withoutftest.
+End InstPat.
diff --git a/test-suite/typeclasses/open_constr.v b/test-suite/typeclasses/open_constr.v
new file mode 100644
index 000000000..5f1785c70
--- /dev/null
+++ b/test-suite/typeclasses/open_constr.v
@@ -0,0 +1,12 @@
+Tactic Notation "opose" open_constr(foo) := pose foo.
+Class Foo := Build_Foo : Set.
+Axiom f : forall `{Foo}, Set.
+Set Printing Implicit.
+Goal forall `{Foo}, True.
+Proof.
+  intro H.
+  pose f.
+  opose f.
+  Fail let x := (eval hnf in P) in has_evar x.
+  let x := (eval hnf in P0) in has_evar x.
+
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index 0e8d224e4..44c83be46 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -314,11 +314,11 @@ type program_info_aux = {
   prg_sign: named_context_val;
 }
 
-type program_info = program_info_aux Ephemeron.key
+type program_info = program_info_aux CEphemeron.key
 
 let get_info x =
-  try Ephemeron.get x
-  with Ephemeron.InvalidKey ->
+  try CEphemeron.get x
+  with CEphemeron.InvalidKey ->
     Errors.anomaly Pp.(str "Program obligation can't be accessed by a worker")
 
 let assumption_message = Declare.assumption_message
@@ -451,7 +451,7 @@ let subst_deps_obl obls obl =
 
 module ProgMap = Map.Make(Id)
 
-let map_replace k v m = ProgMap.add k (Ephemeron.create v) (ProgMap.remove k m)
+let map_replace k v m = ProgMap.add k (CEphemeron.create v) (ProgMap.remove k m)
 
 let map_keys m = ProgMap.fold (fun k _ l -> k :: l) m []
 
@@ -675,7 +675,7 @@ let init_prog_info ?(opaque = false) sign n pl b t ctx deps fixkind
 let map_cardinal m =
   let i = ref 0 in
   ProgMap.iter (fun _ v ->
-		if snd (Ephemeron.get v).prg_obligations > 0 then incr i) m;
+		if snd (CEphemeron.get v).prg_obligations > 0 then incr i) m;
   !i
 
 exception Found of program_info
@@ -683,7 +683,7 @@ exception Found of program_info
 let map_first m =
   try
     ProgMap.iter (fun _ v ->
-		  if snd (Ephemeron.get v).prg_obligations > 0 then
+		  if snd (CEphemeron.get v).prg_obligations > 0 then
 		    raise (Found v)) m;
     assert(false)
   with Found x -> x
@@ -1040,7 +1040,7 @@ let add_definition n ?term t ctx ?pl ?(implicits=[]) ?(kind=Global,false,Definit
   else (
     let len = Array.length obls in
     let _ = Flags.if_verbose msg_info (info ++ str ", generating " ++ int len ++ str " obligation(s)") in
-      progmap_add n (Ephemeron.create prg);
+      progmap_add n (CEphemeron.create prg);
       let res = auto_solve_obligations (Some n) tactic in
 	match res with
 	| Remain rem -> Flags.if_verbose (fun () -> show_obligations ~msg:false (Some n)) (); res
@@ -1054,7 +1054,7 @@ let add_mutual_definitions l ctx ?pl ?tactic ?(kind=Global,false,Definition) ?(r
     (fun  (n, b, t, imps, obls) ->
      let prg = init_prog_info sign ~opaque n pl (Some b) t ctx deps (Some fixkind)
        notations obls imps kind reduce hook 
-     in progmap_add n (Ephemeron.create prg)) l;
+     in progmap_add n (CEphemeron.create prg)) l;
     let _defined =
       List.fold_left (fun finished x ->
 	if finished then finished