From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 28 Apr 2006 14:59:16 +0000
Subject: Imported Upstream version 8.0pl3+8.1alpha

---
 tactics/dhyp.ml | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

(limited to 'tactics/dhyp.ml')

diff --git a/tactics/dhyp.ml b/tactics/dhyp.ml
index fb672d0b..511e0950 100644
--- a/tactics/dhyp.ml
+++ b/tactics/dhyp.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: dhyp.ml,v 1.30.2.1 2004/07/16 19:30:52 herbelin Exp $ *)
+(* $Id: dhyp.ml 7732 2005-12-26 13:51:24Z herbelin $ *)
 
 (* Chet's comments about this tactic :
  
@@ -129,7 +129,6 @@ open Libobject
 open Library
 open Pattern
 open Matching
-open Ast
 open Pcoq
 open Tacexpr
 open Libnames
@@ -266,11 +265,10 @@ let match_dpat dp cls gls =
     | ({onhyps=lo;onconcl=false},HypLocation(_,hypd,concld)) ->
         let hl = match lo with
             Some l -> l
-          | None -> List.map (fun id -> (id,[],(InHyp,ref None)))
-                     (pf_ids_of_hyps gls) in
+          | None -> List.map (fun id -> (id,[],InHyp)) (pf_ids_of_hyps gls) in
         if not
           (List.for_all
-            (fun (id,_,(hl,_)) ->
+            (fun (id,_,hl) ->
               let cltyp = pf_get_hyp_typ gls id in
               let cl = pf_concl gls in
               (hl=InHyp) &
-- 
cgit v1.2.3