From 7df139ca0834b0b93e6259eaecb05c0b8c5cbe99 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 10 May 2008 15:38:36 +0000
Subject: - Prise en compte de l'unicode dans la fonction hdchar (elle
 fournissait des   noms illégaux si le type auquel elle s'appliquait n'était
 pas pur ascii).   [util.ml, termops.ml] - Simplification de la procédure
 d'initialisation (apparemment des résidus   obsolètes de la V5.10) et
 messages d'erreurs [lib.ml, toplevel.ml, coqtop.ml] - Quelques
 pattern-matching incomplets [topconstr.ml, detyping.ml]

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

(limited to 'interp')

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index cad9ad602e..081c2117b5 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -347,7 +347,8 @@ 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 _ | Evd.GoalEvar ) -> raw
+    | Evd.InternalHole | Evd.TomatchTypeParameter _ | Evd.GoalEvar
+    | Evd.ImpossibleCase) -> raw
 
   | ACast (r1,k) -> 
       match k with
-- 
cgit v1.2.3