diff options
| author | herbelin | 2000-10-06 16:08:20 +0000 |
|---|---|---|
| committer | herbelin | 2000-10-06 16:08:20 +0000 |
| commit | 970b4b750486ad8544b5d0a3b2246282690e6c98 (patch) | |
| tree | d8aeeee6133883547e7e30246fcc544e32ae9746 /library | |
| parent | ca91e3c69ba2dfed3f8fd24f721873f5d0cd2004 (diff) | |
Correction incompatibilites dans la fn des types des inductifs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@673 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/global.ml | 5 | ||||
| -rw-r--r-- | library/global.mli | 4 | ||||
| -rw-r--r-- | library/impargs.ml | 4 |
3 files changed, 7 insertions, 6 deletions
diff --git a/library/global.ml b/library/global.ml index e58f1b03b9..96fb689a34 100644 --- a/library/global.ml +++ b/library/global.ml @@ -66,7 +66,8 @@ let mind_is_recursive = let mind_nconstr = Util.compose Inductive.mis_nconstr lookup_mind_specif let mind_nparams = Util.compose Inductive.mis_nparams lookup_mind_specif -let mind_arity = Util.compose Inductive.mis_arity lookup_mind_specif -let mind_lc = Util.compose Inductive.mis_lc lookup_mind_specif +let mind_nf_arity x = + body_of_type (Inductive.mis_user_arity (lookup_mind_specif x)) +let mind_nf_lc = Util.compose Inductive.mis_nf_lc lookup_mind_specif diff --git a/library/global.mli b/library/global.mli index 4a993d1aaa..16ed53785f 100644 --- a/library/global.mli +++ b/library/global.mli @@ -56,6 +56,6 @@ val id_of_global : global_reference -> identifier val mind_is_recursive : inductive -> bool val mind_nconstr : inductive -> int val mind_nparams : inductive -> int -val mind_arity : inductive -> constr -val mind_lc : inductive -> constr array +val mind_nf_arity : inductive -> constr +val mind_nf_lc : inductive -> constr array diff --git a/library/impargs.ml b/library/impargs.ml index 242b634f74..b756a1f99b 100644 --- a/library/impargs.ml +++ b/library/impargs.ml @@ -67,8 +67,8 @@ let inductives_table = ref Spmap.empty let declare_inductive_implicits sp = let mib = Global.lookup_mind sp in let imps_one_inductive mip = - (auto_implicits (mind_user_arity mip), - Array.map (fun c -> auto_implicits c) (mind_user_lc mip)) + (auto_implicits (body_of_type (mind_user_arity mip)), + Array.map (fun c -> auto_implicits (body_of_type c)) (mind_user_lc mip)) in let imps = Array.map imps_one_inductive mib.mind_packets in inductives_table := Spmap.add sp imps !inductives_table |