From bdec9fddcdaa13800e04e718ffa52f87bddc52d9 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Thu, 8 Oct 2009 13:10:30 +0000
Subject: Implicit argument of Logic.eq become maximally inserted

  This allow in particular to write eq instead of (@eq _) in
  signatures of morphisms. I dont really see how this could
  break existing code, no change in the stdlib was mandatory.
  We'll check the contribs tomorrow...

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12379 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Logic.v | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'theories/Init')

diff --git a/theories/Init/Logic.v b/theories/Init/Logic.v
index ede73ebf14..e1bb443a63 100644
--- a/theories/Init/Logic.v
+++ b/theories/Init/Logic.v
@@ -251,6 +251,8 @@ Notation "x = y" := (x = y :>_) : type_scope.
 Notation "x <> y  :> T" := (~ x = y :>T) : type_scope.
 Notation "x <> y" := (x <> y :>_) : type_scope.
 
+Implicit Arguments eq [ [A] ].
+
 Implicit Arguments eq_ind [A].
 Implicit Arguments eq_rec [A].
 Implicit Arguments eq_rect [A].
-- 
cgit v1.2.3