From 28a551e49864bbfee8a9212fdbcc364d1132b19e Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 29 May 2007 10:01:06 +0000
Subject: Correction d'un bug dans l'affichage du message d'erreur real_clean
 (cas d'un terme sans Rel libre), introduction au passage d'un nouveau type
 d'evar EvarGoal pour raffinement du message d'erreur.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9868 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/topconstr.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 514c0811c7..0c5e6dbaed 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -348,7 +348,7 @@ let rec subst_aconstr subst bound raw =
 	if ref' == ref then raw else
 	  AHole (Evd.InternalHole)
   | AHole (Evd.BinderType _ | Evd.QuestionMark _ | Evd.CasesType 
-    | Evd.InternalHole | Evd.TomatchTypeParameter _) -> raw
+    | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar ) -> raw
 
   | ACast (r1,k) -> 
       match k with
-- 
cgit v1.2.3