From b098dbfa1d910224a2cbb16f95f0b47e88ab69dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 12 Dec 2006 10:39:13 +0000
Subject: 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
---
 theories/Logic/ChoiceFacts.v | 14 ++++----------
 1 file changed, 4 insertions(+), 10 deletions(-)

diff --git a/theories/Logic/ChoiceFacts.v b/theories/Logic/ChoiceFacts.v
index 76807b06bb..75043c4229 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.
 
-- 
cgit v1.2.3