diff options
| author |  amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 15:40:04 +0000 |
|---|---|---|
| committer | amahboub <amahboub@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2013-08-22 15:40:04 +0000 |
| commit | eb4bbd580ebcb9b2f03f9d8313b6de26819dedf7 (patch) | |
| tree | 0a08734658234dd7e3f0541dd1e1bedc663cf2d6 /plugins/setoid_ring/Field_theory.v | |
| parent | 80f974b1cc399759c5e90a653bdccc3e1d508cbd (diff) | |
Correcting misplaced Proof command.
I did not even know it was possible to inline a 'Proof.'
anywhere in a script.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16729 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/setoid_ring/Field_theory.v')
| -rw-r--r-- | plugins/setoid_ring/Field_theory.v | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/plugins/setoid_ring/Field_theory.v b/plugins/setoid_ring/Field_theory.v index 52b632a7d..bc947d54e 100644 --- a/plugins/setoid_ring/Field_theory.v +++ b/plugins/setoid_ring/Field_theory.v @@ -1396,13 +1396,14 @@ Fixpoint Fapp (l m:list (PExpr C)) {struct l} : list (PExpr C) := Lemma fcons_ok : forall 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. +intros l l1 h1; assert (H := h1 (PCond l) (refl_equal _));clear h1. 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. |