From 900d95913b625f9a7483dfefbf7ea0fbf93bcea2 Mon Sep 17 00:00:00 2001
From: barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Fri, 3 Sep 2004 18:56:25 +0000
Subject: deplacement de clenv vers pretyping

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/logic.mli | 1 -
 1 file changed, 1 deletion(-)

(limited to 'proofs/logic.mli')

diff --git a/proofs/logic.mli b/proofs/logic.mli
index 34e5b9e98..0a641e975 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -54,7 +54,6 @@ type refiner_error =
   | NonLinearProof of constr
 
   (*i Errors raised by the tactics i*)
-  | CannotUnifyBindingType of constr * constr
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
 
-- 
cgit v1.2.3