diff options
| author | herbelin | 2000-07-01 17:53:48 +0000 |
|---|---|---|
| committer | herbelin | 2000-07-01 17:53:48 +0000 |
| commit | a51f67a717a93cf61bfed79e70da9f35555dcab7 (patch) | |
| tree | 34789ed013f1edd5669f2db84bff8cddb63567a8 /toplevel | |
| parent | c6edcac49bc32e12106e576430c3251d78276f8e (diff) | |
Précalcul de la forme canonique des constructeurs et arités pour traiter les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/discharge.ml | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml index da223b541a..ebf70569db 100644 --- a/toplevel/discharge.ml +++ b/toplevel/discharge.ml @@ -207,9 +207,17 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib = array_map_to_list (fun mip -> (mip.mind_typename, - expmod_type oldenv modlist mip.mind_arity, + make_typed_lazy + (expmod_constr oldenv modlist (mind_user_arity mip)) + (fun _ -> level_of_type mip.mind_nf_arity), Array.to_list mip.mind_consnames, - array_map_to_list (expmod_type oldenv modlist) mip.mind_lc)) + 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))) mib.mind_packets in let (inds',modl) = abstract_inductive ids_to_discard mib.mind_hyps inds in |