diff options
| author | sacerdot | 2005-01-14 14:30:06 +0000 |
|---|---|---|
| committer | sacerdot | 2005-01-14 14:30:06 +0000 |
| commit | b5657ff1939c6872ee3ccaeaf180a2f3da9e1876 (patch) | |
| tree | 329838825dc03d431fc36489fdc818ca04d4bd2a /contrib/first-order | |
| parent | 6dbc9f181b90216958fd9d87f8426901b1e4c37e (diff) | |
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
Diffstat (limited to 'contrib/first-order')
| -rw-r--r-- | contrib/first-order/formula.ml | 4 |
1 files changed, 2 insertions, 2 deletions
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 |