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/xml | |
| 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/xml')
| -rw-r--r-- | contrib/xml/cic2acic.ml | 4 | ||||
| -rw-r--r-- | contrib/xml/doubleTypeInference.ml | 4 | ||||
| -rw-r--r-- | contrib/xml/xmlcommand.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/contrib/xml/cic2acic.ml b/contrib/xml/cic2acic.ml index dca5963f9a..10a428e832 100644 --- a/contrib/xml/cic2acic.ml +++ b/contrib/xml/cic2acic.ml @@ -243,9 +243,9 @@ let typeur sigma metamap = let cb = Environ.lookup_constant c env in T.body_of_type cb.Declarations.const_type | T.Evar ev -> Evd.existential_type sigma ev - | T.Ind ind -> T.body_of_type (Inductive.type_of_inductive env ind) + | T.Ind ind -> T.body_of_type (Inductiveops.type_of_inductive env ind) | T.Construct cstr -> - T.body_of_type (Inductive.type_of_constructor env cstr) + T.body_of_type (Inductiveops.type_of_constructor env cstr) | T.Case (_,p,c,lf) -> let Inductiveops.IndType(_,realargs) = try Inductiveops.find_rectype env sigma (type_of env c) diff --git a/contrib/xml/doubleTypeInference.ml b/contrib/xml/doubleTypeInference.ml index 728c7ac9a7..d4093f002c 100644 --- a/contrib/xml/doubleTypeInference.ml +++ b/contrib/xml/doubleTypeInference.ml @@ -124,10 +124,10 @@ let double_type_of env sigma cstr expectedty subterms_to_types = E.make_judge cstr (E.constant_type env c) | T.Ind ind -> - E.make_judge cstr (Inductive.type_of_inductive env ind) + E.make_judge cstr (Inductiveops.type_of_inductive env ind) | T.Construct cstruct -> - E.make_judge cstr (Inductive.type_of_constructor env cstruct) + E.make_judge cstr (Inductiveops.type_of_constructor env cstruct) | T.Case (ci,p,c,lf) -> let expectedtype = diff --git a/contrib/xml/xmlcommand.ml b/contrib/xml/xmlcommand.ml index f448dd4ed1..41967dede6 100644 --- a/contrib/xml/xmlcommand.ml +++ b/contrib/xml/xmlcommand.ml @@ -406,7 +406,7 @@ let mk_inductive_obj sp packs variables hyps finite = D.mind_typename=typename ; D.mind_nf_arity=arity} = p in - let lc = Inductive.arities_of_constructors (Global.env ()) (sp,!tyno) in + let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in let cons = (Array.fold_right (fun (name,lc) i -> (name,lc)::i) (Array.mapi |