diff options
| author | letouzey | 2006-05-30 21:32:10 +0000 |
|---|---|---|
| committer | letouzey | 2006-05-30 21:32:10 +0000 |
| commit | 5514d654d2d8b29a46d65d0f38bdf36a69c56f45 (patch) | |
| tree | 1d51ec0ed0d14f493fd55ad1f75692566c451478 /kernel/modops.ml | |
| parent | deb036a1712e802a55a6160630387fb52ce3d998 (diff) | |
retour au comportement antérieur pour une application de foncteur:
plus d'expansions, un foncteur F dependant de X donne une fois
appliquee a M un module dont le corps est simplement celui de F
avec des M a la place des X.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8879 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/modops.ml')
| -rw-r--r-- | kernel/modops.ml | 32 |
1 files changed, 5 insertions, 27 deletions
diff --git a/kernel/modops.ml b/kernel/modops.ml index 5fece5b1fd..aacc8f30c2 100644 --- a/kernel/modops.ml +++ b/kernel/modops.ml @@ -190,35 +190,13 @@ and constants_of_modtype env mp modtype = (subst_signature_msid msid mp sign) | MTBfunsig _ -> [] -(* returns a resolver for kn that maps mbid to mp and then delta-expands - the obtained constants according to env *) +(* returns a resolver for kn that maps mbid to mp *) +(* Nota: Some delta-expansions used to happen here. + Browse SVN if you want to know more. *) let resolver_of_environment mbid modtype mp env = let constants = constants_of_modtype env (MPbound mbid) modtype in - let resolve = - List.map - (fun (con,expecteddef) -> - let con' = replace_mp_in_con (MPbound mbid) mp con in - let constr = - try - if expecteddef.Declarations.const_body <> None then - (* Do not expand constants that already have a body in the - expected type (i.e. only parameters/axioms in the module type - are expanded). In the few examples we have this seems to - be the more reasonable behaviour for the user. *) - None - else - let constant = lookup_constant con' env in - if constant.Declarations.const_opaque then - None - else - option_map Declarations.force - constant.Declarations.const_body - with Not_found -> error_no_such_label (con_label con') - in - con,constr - ) constants - in - Mod_subst.make_resolver resolve + let resolve = List.map (fun (con,_) -> con,None) constants in + Mod_subst.make_resolver resolve (* we assume that the substitution of "mp" into "msid" is already done (or unnecessary) *) |