--- a/src/MoreSpecif.v	Mon Oct 27 10:31:57 2008 -0400
+++ b/src/MoreSpecif.v	Tue Oct 28 11:29:14 2008 -0400
@@ -73,3 +73,22 @@
 
 Notation "e1 ;;; e2" := (if e1 then e2 else !!)
   (right associativity, at level 60) : specif_scope.
+
+
+Section partial.
+  Variable P : Prop.
+
+  Inductive partial : Set :=
+  | Proved : P -> partial
+  | Uncertain : partial.
+End partial.
+
+Notation "[ P ]" := (partial P) : type_scope.
+
+Notation "'Yes'" := (Proved _) : partial_scope.
+Notation "'No'" := (Uncertain _) : partial_scope.
+
+Open Local Scope partial_scope.
+Delimit Scope partial_scope with partial.
+
+Notation "'Reduce' v" := (if v then Yes else No) : partial_scope.