From 87cc9ecc0232a37de19774208689bf9be0c293d7 Mon Sep 17 00:00:00 2001
From: coq
Date: Fri, 17 Feb 2006 00:40:32 +0000
Subject: changed the decomposition of an induction scheme

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

(limited to 'contrib')

diff --git a/contrib/funind/invfun.ml b/contrib/funind/invfun.ml
index a8429d3c47..4e87c4c958 100644
--- a/contrib/funind/invfun.ml
+++ b/contrib/funind/invfun.ml
@@ -3,10 +3,10 @@ open Names
 open Term
 open Tacinvutils
 open Pp
-open Indfun_common
 open Libnames
 open Tacticals
 open Tactics
+open Indfun_common
 open Tacmach
 open Sign
 
@@ -107,7 +107,7 @@ let invfun (hypname:identifier) (fid:identifier) : tactic=
 	     )
 	 with _ -> assert false)
       in
-      compute_elim_sig princ_type
+      Indfun_common.compute_elim_sig princ_type
     in
     let _,_,typhyp = List.find (fun (id,_,_) -> hypname=id) (pf_hyps g) in
     let do_invert  fargs  appf : tactic = 
-- 
cgit v1.2.3