From ddca52206138c9e0da46c38d6cec052628d0d7da Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 22 Jun 2007 08:05:11 +0000
Subject: Ajout exist & cie à la table des hints par symétrie avec ex_intro &
 cie (cf message coq-club 21/6/07). De plus, left/right inleft/inright, eux
 aussi dans Set/Type, y étaient déjà donc l'argument d'être dans Type n'est
 pas recevable.

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

diff --git a/theories/Init/Specif.v b/theories/Init/Specif.v
index 5bf9621b14..9495cb707f 100644
--- a/theories/Init/Specif.v
+++ b/theories/Init/Specif.v
@@ -201,6 +201,7 @@ Proof.
 Qed.
 
 Hint Resolve left right inleft inright: core v62.
+Hint Resolve exist exist2 existT existT2: core.
 
 (* Compatibility *)
 
-- 
cgit v1.2.3