From deb036a1712e802a55a6160630387fb52ce3d998 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 30 May 2006 16:44:25 +0000
Subject: Généralisation de with_occurrence (ex occurrence) et de red_expr pour
 permettre de passer les occurrences en paramètre dans ltac, par exemple à
 pattern

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

(limited to 'contrib/funind')

diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index 85a60bd1c0..2e5616f0e1 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -105,7 +105,7 @@ let invfun (hypname:identifier) fname princ : tactic=
       let frealargs = (snd (array_chop (List.length princ_info.params) fargs))  
       in
       let pat_args = 
-	(List.map (fun e -> ([-1],e)) (Array.to_list frealargs)) @ [[],appf] 
+	(List.map (fun e -> ([Rawterm.ArgArg (-1)],e)) (Array.to_list frealargs)) @ [[],appf] 
       in
       tclTHENSEQ 
 	[
-- 
cgit v1.2.3