From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001
From: Stephane Glondu <steph@glondu.net>
Date: Thu, 12 Jan 2012 16:02:20 +0100
Subject: Imported Upstream version 8.4~beta

---
 theories/Init/Specif.v | 36 ++++++++++++++++++++----------------
 1 file changed, 20 insertions(+), 16 deletions(-)

(limited to 'theories/Init/Specif.v')

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 5a951d14..637994b2 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -1,13 +1,11 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: Specif.v 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
 (** Basic specifications : sets that may contain logical information *)
 
 Set Implicit Arguments.
@@ -40,10 +38,10 @@ Inductive sigT2 (A:Type) (P Q:A -> Type) : Type :=
 
 (* Notations *)
 
-Arguments Scope sig [type_scope type_scope].
-Arguments Scope sig2 [type_scope type_scope type_scope].
-Arguments Scope sigT [type_scope type_scope].
-Arguments Scope sigT2 [type_scope type_scope type_scope].
+Arguments sig (A P)%type.
+Arguments sig2 (A P Q)%type.
+Arguments sigT (A P)%type.
+Arguments sigT2 (A P Q)%type.
 
 Notation "{ x  |  P }" := (sig (fun x => P)) : type_scope.
 Notation "{ x  |  P  & Q }" := (sig2 (fun x => P) (fun x => Q)) : type_scope.
@@ -128,6 +126,9 @@ Inductive sumbool (A B:Prop) : Set :=
 
 Add Printing If sumbool.
 
+Arguments left {A B} _, [A] B _.
+Arguments right {A B} _ , A [B] _.
+
 (** [sumor] is an option type equipped with the justification of why
     it may not be a regular value *)
 
@@ -138,6 +139,9 @@ Inductive sumor (A:Type) (B:Prop) : Type :=
 
 Add Printing If sumor.
 
+Arguments inleft {A B} _ , [A] B _.
+Arguments inright {A B} _ , A [B] _.
+
 (** Various forms of the axiom of choice for specifications *)
 
 Section Choice_lemmas.
@@ -152,16 +156,16 @@ Section Choice_lemmas.
   Proof.
    intro H.
    exists (fun z => proj1_sig (H z)).
-   intro z; destruct (H z); trivial.
-  Qed.
+   intro z; destruct (H z); assumption.
+  Defined.
 
   Lemma Choice2 :
    (forall x:S, {y:S' & R' x y}) -> {f:S -> S' & forall z:S, R' z (f z)}.
   Proof.
     intro H.
     exists (fun z => projT1 (H z)).
-    intro z; destruct (H z); trivial.
-  Qed.
+    intro z; destruct (H z); assumption.
+  Defined.
 
   Lemma bool_choice :
    (forall x:S, {R1 x} + {R2 x}) ->
@@ -170,7 +174,7 @@ Section Choice_lemmas.
     intro H.
     exists (fun z:S => if H z then true else false).
     intro z; destruct (H z); auto.
-  Qed.
+  Defined.
 
 End Choice_lemmas.
 
@@ -188,7 +192,7 @@ Section Dependent_choice_lemmas.
     exists f.
     split. reflexivity.
     induction n; simpl; apply proj2_sig.
-  Qed.
+  Defined.
 
 End Dependent_choice_lemmas.
 
@@ -204,18 +208,18 @@ Definition Exc := option.
 Definition value := Some.
 Definition error := @None.
 
-Implicit Arguments error [A].
+Arguments error [A].
 
 Definition except := False_rec. (* for compatibility with previous versions *)
 
-Implicit Arguments except [P].
+Arguments except [P] _.
 
 Theorem absurd_set : forall (A:Prop) (C:Set), A -> ~ A -> C.
 Proof.
   intros A C h1 h2.
   apply False_rec.
   apply (h2 h1).
-Qed.
+Defined.
 
 Hint Resolve left right inleft inright: core v62.
 Hint Resolve exist exist2 existT existT2: core.
-- 
cgit v1.2.3