1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v
index d584adfc8..52b632a7d 100644
--- a/plugins/setoid_ring/Field_theory.v
+++ b/plugins/setoid_ring/Field_theory.v
@@ -1395,14 +1395,14 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) :=
   end.
 
 Lemma fcons_ok : forall l l1,
-  PCond l (Fapp l1 nil) -> PCond l l1.
+  (forall lock, lock = PCond l -> lock (Fapp l1 nil)) -> PCond l l1.
+intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1.
 Proof.
 induction l1; simpl; intros.
  trivial.
  elim PCond_fcons_inv with (1 := H); intros.
  destruct l1; trivial. split; trivial. apply IHl1; trivial.
 Qed.
-
 End Fcons_impl.
 
 Section Fcons_simpl.