diff --git a/theories/base_logic/lib/own.v b/theories/base_logic/lib/own.v
index 0c49790826b31f5a487fd92bbb2f187c9b93594c..fb6601ad17a05177ceda026a7058bc4615af5f79 100644
--- a/theories/base_logic/lib/own.v
+++ b/theories/base_logic/lib/own.v
@@ -45,12 +45,12 @@ Ltac solve_inG :=
   repeat match goal with
          | H : subG _ _ |- _ => move:(H); (apply subG_inG in H || clear H)
          end;
-  (* Again get all assumptions *)
-  intros;
+  (* Again get all assumptions and simplify the functors *)
+  intros; simpl in *;
   (* We support two kinds of goals: Things convertible to inG;
      and records with inG and typeclass fields. Try to solve the
      first case. *)
-  try done;
+  try assumption;
   (* That didn't work, now we're in for the second case. *)
   split; (assumption || by apply _).