diff options
| -rw-r--r-- | plugins/setoid_ring/Field_tac.v | 2 | ||||
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 4 |
2 files changed, 3 insertions, 3 deletions
diff --git a/plugins/setoid_ring/Field_tac.v b/plugins/setoid_ring/Field_tac.v index c46e7a933..dda1edbe1 100644 --- a/plugins/setoid_ring/Field_tac.v +++ b/plugins/setoid_ring/Field_tac.v @@ -201,7 +201,7 @@ Ltac fold_field_cond req := Ltac simpl_PCond FLD := let req := get_FldEq FLD in let lemma := get_CondLemma FLD in - try apply lemma; + try (apply lemma; intros lock lock_def; vm_compute; rewrite lock_def; clear lock_def lock); protect_fv "field_cond"; fold_field_cond req; try exact I. 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. |