From ccff0b020b3a0950a6358846b6a40b8cd7a96562 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 18 Jul 2008 10:06:36 +0000
Subject: Modification rapide du message d'erreur lorsqu'un _ ne peut être
 effacé dans un intro-pattern (suggéré par ssreflect).

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

(limited to 'proofs')

diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7fd7aabe40..8e3e48d4fc 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -8,6 +8,7 @@
 
 (* $Id$ *)
 
+open Pp
 open Util
 open Names
 open Nameops
@@ -226,11 +227,21 @@ let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
 let refine c           = with_check (refine_no_check c)
 let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
-let thin l             = with_check (thin_no_check l)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
 let rename_hyp l       = with_check (rename_hyp_no_check l)
 
+let thin l gl = 
+  try with_check (thin_no_check l) gl
+  with Evarutil.OccurHypInSimpleClause (id,ido) ->
+    match ido with
+    | None ->
+	errorlabstrm "" (pr_id id ++ str " is used in conclusion.")
+    | Some id' -> 
+	errorlabstrm "" 
+	 (pr_id id ++ strbrk " is used in hypothesis " ++ pr_id id' ++ str ".")
+
+
 (* Pretty-printers *)
 
 open Pp
-- 
cgit v1.2.3