From b5657ff1939c6872ee3ccaeaf180a2f3da9e1876 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Fri, 14 Jan 2005 14:30:06 +0000
Subject: Inductive.{type_of_inductive,type_of_constructor,arities_of_specif}
 changed to accept a mind_specif (a couple mutual_inductive_body *
 one_inductive_body) instead of looking it up in the environment. A version of
 the same functions with the old type is put in Inductiveops (outside the
 kernel).

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

(limited to 'contrib/first-order')

diff --git a/contrib/first-order/formula.ml b/contrib/first-order/formula.ml
index 8b5c30521e..9dbda969a1 100644
--- a/contrib/first-order/formula.ml
+++ b/contrib/first-order/formula.ml
@@ -48,13 +48,13 @@ let rec nb_prod_after n c=
 let construct_nhyps ind gls =
   let env=pf_env gls in
   let nparams = (snd (Global.lookup_inductive ind)).mind_nparams in
-  let constr_types = Inductive.arities_of_constructors (pf_env gls) ind in 
+  let constr_types = Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let hyp = nb_prod_after nparams in	
     Array.map hyp constr_types
 
 (* indhyps builds the array of arrays of constructor hyps for (ind largs)*)
 let ind_hyps nevar ind largs gls= 
-  let types= Inductive.arities_of_constructors (pf_env gls) ind in 
+  let types= Inductiveops.arities_of_constructors (pf_env gls) ind in 
   let lp=Array.length types in     
   let myhyps i=
     let t1=Term.prod_applist types.(i) largs in
-- 
cgit v1.2.3