diff options
| -rw-r--r-- | theories/Init/Specif.v | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v index 6025078673..12ac08ff0c 100644 --- a/theories/Init/Specif.v +++ b/theories/Init/Specif.v @@ -139,6 +139,9 @@ Inductive sumor (A:Type) (B:Prop) : Type := Add Printing If sumor. +Implicit Arguments inleft [[A] [B]] [A]. +Implicit Arguments inright [[A] [B]] [B]. + (** Various forms of the axiom of choice for specifications *) Section Choice_lemmas. |