From 225b988abb80dbc2b1508ac2aecce65a330f03e5 Mon Sep 17 00:00:00 2001
From: sacerdot
Date: Wed, 5 Jan 2005 13:26:02 +0000
Subject: [ Waiting for a keyword to control expansion during functor
 application ] When F(X: T) := B is applied to M, M.t in B{M/X} is now
 delta-expanded only if T.t is an axiom or a parameter. This seems to be the
 expected behaviour at least for orsay/FSets.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6561 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/modops.ml | 23 +++++++++++++++--------
 1 file changed, 15 insertions(+), 8 deletions(-)

(limited to 'kernel/modops.ml')

diff --git a/kernel/modops.ml b/kernel/modops.ml
index 2808973fa6..744da223a9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -168,7 +168,7 @@ let subst_signature_msid msid mp =
 let rec constants_of_specification env mp sign =
  let aux res (l,elem) =
   match elem with
-   | SPBconst cb -> (make_con mp empty_dirpath l)::res
+   | SPBconst cb -> ((make_con mp empty_dirpath l),cb)::res
    | SPBmind _ -> res
    | SPBmodule mb ->
       (constants_of_modtype env (MPdot (mp,l))
@@ -191,16 +191,23 @@ let resolver_of_environment mbid modtype mp env =
  let constants = constants_of_modtype env (MPbound mbid) modtype in
  let resolve =
   List.map
-   (fun con ->
+   (fun (con,expecteddef) ->
      let con' = replace_mp_in_con (MPbound mbid) mp con in
      let constr =
       try
-       let constant = lookup_constant con' env in
-        if constant.Declarations.const_opaque then
-         None
-        else
-         option_app Declarations.force
-          constant.Declarations.const_body
+       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_app Declarations.force
+           constant.Declarations.const_body
       with Not_found -> assert false
      in
       con,constr
-- 
cgit v1.2.3