From 32f49f477bd620e4754de14f1c5a1eab707307f5 Mon Sep 17 00:00:00 2001
From: puech
Date: Fri, 29 Jul 2011 14:24:27 +0000
Subject: Hipattern: two generic equalities on constr spotted & rewritten

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14316 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/hipattern.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tactics/hipattern.ml4 b/tactics/hipattern.ml4
index f0773f793d..9057c60d3c 100644
--- a/tactics/hipattern.ml4
+++ b/tactics/hipattern.ml4
@@ -95,7 +95,7 @@ let match_with_one_constructor style allow_rec t =
 	      (decompose_prod_n_assum mib.mind_nparams mip.mind_nf_lc.(0)))) in
 	  if
 	    List.for_all
-	      (fun (_,b,c) -> b=None && c = mkRel mib.mind_nparams) ctx
+	      (fun (_,b,c) -> b=None && isRel c && destRel c = mib.mind_nparams) ctx
 	  then
 	    Some (hdapp,args)
 	  else None
@@ -142,7 +142,7 @@ let is_tuple t =
 let test_strict_disjunction n lc =
   array_for_all_i (fun i c ->
     match (prod_assum (snd (decompose_prod_n_assum n c))) with
-    | [_,None,c] -> c = mkRel (n - i)
+    | [_,None,c] -> isRel c && destRel c = (n - i)
     | _ -> false) 0 lc
 
 let match_with_disjunction ?(strict=false) t =
-- 
cgit v1.2.3