From aa3b44033ede838336b6adc08d0e0662552fa90d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 11 Jan 2006 11:40:05 +0000
Subject: Résidus du traducteur v7 -> v8

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

diff --git a/interp/topconstr.ml b/interp/topconstr.ml
index 2f2a381c04..60e117d9ea 100644
--- a/interp/topconstr.ml
+++ b/interp/topconstr.ml
@@ -433,7 +433,6 @@ let rec match_ alp metas sigma a1 a2 = match (a1,a2) with
   | RSort (_,s1), ASort s2 when s1 = s2 -> sigma
   | RPatVar _, AHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
   | a, AHole _ -> sigma
-  | RHole _, AHole _ -> sigma
   | (RDynamic _ | RRec _ | REvar _), _ 
   | _,_ -> raise No_match
 
-- 
cgit v1.2.3