diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:08:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2000-10-06 16:08:20 +0000 |
| commit | 970b4b750486ad8544b5d0a3b2246282690e6c98 (patch) | |
| tree | d8aeeee6133883547e7e30246fcc544e32ae9746 /toplevel | |
| 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 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 11 |
1 files changed, 2 insertions, 9 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index dc6f01d34..805e4ffc0 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -230,17 +230,10 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = array_map_to_list (fun mip -> (mip.mind_typename, - make_typed_lazy - (expmod_constr oldenv modlist (mind_user_arity mip)) - (fun _ -> level_of_type mip.mind_nf_arity), + expmod_type oldenv modlist (mind_user_arity mip), Array.to_list mip.mind_consnames, Array.to_list - (array_map2 - (fun us nfc -> - make_typed_lazy - (expmod_constr oldenv modlist us) - (fun _ -> level_of_type nfc)) - (mind_user_lc mip) mip.mind_nf_lc))) + (Array.map (expmod_type oldenv modlist) (mind_user_lc mip)))) mib.mind_packets in let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in |