Fixing unification regression #5323.

Tracking conversion problems to reconsider was lost for evars subject
to restriction (field last_mods was not updated and conversion
problems not considered to be changed).

2 files changed, 30 insertions, 1 deletions

diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 2f4b8fc12f..7b0ffd8b1d 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -898,13 +898,16 @@ let restrict evk evk' filter ?candidates evd =
     { evar_info with evar_filter = filter;
       evar_candidates = candidates;
       evar_extra = Store.empty } in
+  let last_mods = match evd.conv_pbs with
+  | [] ->  evd.last_mods
+  | _ -> Evar.Set.add evk evd.last_mods in
   let evar_names = EvNames.reassign_name_defined evk evk' evd.evar_names in
   let ctxt = Filter.filter_list filter (evar_context evar_info) in
   let id_inst = Array.map_of_list (fun (id,_,_) -> mkVar id) ctxt in
   let body = mkEvar(evk',id_inst) in
   let (defn_evars, undf_evars) = define_aux evd.defn_evars evd.undf_evars evk body in
   { evd with undf_evars = EvMap.add evk' evar_info' undf_evars;
-    defn_evars; evar_names }
+    defn_evars; last_mods; evar_names }
 
 let downcast evk ccl evd =
   let evar_info = EvMap.find evk evd.undf_evars in
diff --git a/test-suite/bugs/closed/5323.v b/test-suite/bugs/closed/5323.v
new file mode 100644
index 0000000000..295b7cd9f5
--- /dev/null
+++ b/test-suite/bugs/closed/5323.v
@@ -0,0 +1,26 @@
+(* Revealed a missing re-consideration of postponed problems *)
+
+Module A.
+Inductive flat_type := Unit | Prod (A B : flat_type).
+Inductive exprf (op : flat_type -> flat_type -> Type) {var : Type} : flat_type 
+-> Type :=
+| Op {t1 tR} (opc : op t1 tR) (args : exprf op t1) : exprf op tR.
+Inductive op : flat_type -> flat_type -> Type := .
+Arguments Op {_ _ _ _} _ _.
+Definition bound_op {var}
+           {src2 dst2}
+           (opc2 : op src2 dst2)
+  : forall (args2 : exprf op (var:=var) src2), Op opc2 args2 = Op opc2 args2
+  := match opc2 return (forall args2, Op opc2 args2 = Op opc2 args2) with end.
+End A.
+
+(* A shorter variant *)
+Module B.
+Inductive exprf (op : unit -> Type) : Type :=
+| A : exprf op
+| Op tR (opc : op tR) (args : exprf op) : exprf op.
+Inductive op : unit -> Type := .
+Definition bound_op (dst2 : unit) (opc2 : op dst2)
+  : forall (args2 : exprf op), Op op dst2 opc2 args2 = A op
+  := match opc2 in op h return (forall args2 : exprf ?[U], Op ?[V] ?[I] opc2 args2 = A op) with end.
+End B.