diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-12 10:39:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-12-12 10:39:13 +0000 |
| commit | b098dbfa1d910224a2cbb16f95f0b47e88ab69dd (patch) | |
| tree | b5a9879a7e392e2dbe30771b425b71b17202bbfd /theories/Logic/ChoiceFacts.v | |
| parent | d2d0b966db4b899ac46d57e6f39b5c3b8c5c3753 (diff) | |
AllÃègement de syntxe suite à l'introduction de l'unif pattern
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9439 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Logic/ChoiceFacts.v')
| -rw-r--r-- | theories/Logic/ChoiceFacts.v | 14 |
1 files changed, 4 insertions, 10 deletions
diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v index 76807b06b..75043c422 100644 --- a/theories/Logic/ChoiceFacts.v +++ b/theories/Logic/ChoiceFacts.v @@ -632,11 +632,8 @@ Proof. destruct (AC_depfun A0 B0 R0 H0) as (f, Hf). apply H. intros A P H'. - exists (f (existT (fun _ => sigT _) A - (existT (fun P => exists x, P x) P H'))). - pose (Hf' := - Hf (existT (fun _ => sigT _) A - (existT (fun P => exists x, P x) P H'))). + exists (f (existT _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed. @@ -664,11 +661,8 @@ Proof. destruct (DepFunReify A0 B0 R0 H0) as (f, Hf). apply H. intros A P H'. - exists (f (existT (fun _ => sigT _) A - (existT (fun P => exists! x, P x) P H'))). - pose (Hf' := - Hf (existT (fun _ => sigT _) A - (existT (fun P => exists! x, P x) P H'))). + exists (f (existT _ A (existT _ P H'))). + pose (Hf' := Hf (existT _ A (existT _ P H'))). assumption. Qed. |