diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Utils.v | 12 |
1 files changed, 10 insertions, 2 deletions
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 *) |