From 144e75ce2835e44542f5d90d751f06243e45ecc4 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Wed, 2 Jan 2008 20:45:37 +0000
Subject: Implicit arguments in class field declarations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10416 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Program/Utils.v | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

(limited to 'theories/Program')

diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v
index 16e8de9707..c514d3234d 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 *)
 
-- 
cgit v1.2.3