From 0dece739c580b39d77708bb8117442e7e1cd560b Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Sat, 21 Dec 2002 11:51:33 +0000
Subject: Légère amélioration des messages d'erreur des with-bindings et des
 Rewrite
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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

(limited to 'proofs/logic.ml')

diff --git a/proofs/logic.ml b/proofs/logic.ml
index 5c95a8e7a..da62c1036 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -42,9 +42,11 @@ type refiner_error =
 
   (* Errors raised by the tactics *)
   | CannotUnify of constr * constr
+  | CannotUnifyBindingType of constr * constr
   | CannotGeneralize of constr
   | IntroNeedsProduct
   | DoesNotOccurIn of constr * identifier
+  | NoOccurrenceFound of constr
 
 exception RefinerError of refiner_error
 
-- 
cgit v1.2.3