Implicit arguments in class field declarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10416 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 10 insertions, 2 deletions

diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 16e8de970..c514d3234 100644
--- a/theories/Program/Utils.v
+++ b/theories/Program/Utils.v
@@ -61,8 +61,16 @@ Notation "'dec'" := (sumbool_of_bool) (at level 0).
 
 (** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *)
 
-Notation in_right := (@right _ _ _).
-Notation in_left := (@left _ _ _).
+
+(** These type arguments should be infered from the context. *)
+
+Implicit Arguments left [[A]].
+Implicit Arguments right [[B]].
+
+(** Hide proofs and generates obligations when put in a term. *)
+
+Notation left := (left _ _).
+Notation right := (right _ _).
 
 (** Extraction directives *)