Pass over Subset

src/MoreDep.v

@@ -993,7 +993,7 @@ Lemma substring_suffix_emp : forall s n m,
   substring n m s = ""
   -> m > 0
   -> n >= length s.
-  destruct m as [| m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
+  destruct m as [ | m]; [crush | intros; apply substring_suffix_emp' with m; assumption].
 Qed.
 
 Hint Rewrite substring_stack substring_stack' substring_suffix

src/MoreSpecif.v

-(* Copyright (c) 2008, Adam Chlipala
+(* Copyright (c) 2008, 2011, Adam Chlipala
  * 
  * This work is licensed under a
  * Creative Commons Attribution-Noncommercial-No Derivative Works 3.0
@@ -51,7 +51,7 @@ Inductive maybe (A : Set) (P : A -> Prop) : Set :=
 
 Notation "{{ x | P }}" := (maybe (fun x => P)) : specif_scope.
 Notation "??" := (Unknown _) : specif_scope.
-Notation "[[ x ]]" := (Found _ x _) : specif_scope.
+Notation "[| x |]" := (Found _ x _) : specif_scope.
 
 Notation "x <- e1 ; e2" := (match e1 with
                              | Unknown => ??
@@ -60,7 +60,7 @@ Notation "x <- e1 ; e2" := (match e1 with
 (right associativity, at level 60) : specif_scope.
 
 Notation "!!" := (inright _ _) : specif_scope.
-Notation "[[[ x ]]]" := (inleft _ [x]) : specif_scope.
+Notation "[|| x ||]" := (inleft _ [x]) : specif_scope.
 
 Notation "x <-- e1 ; e2" := (match e1 with
                                | inright _ => !!