New keyword "Inline" for Parameters and Axioms for automatic

delta-reduction at fonctor application.
Example:

Module Type S.
 Parameter Inline N : Set.
End S.

Module F (X:S).
 Definition t := X.N.
End F.

Module M.
 Definition N := nat.
End M.

Module G := F M.

Print G.t.
G.t = nat
     : Set




git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9795 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 21 insertions, 5 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index e9e1d67eb4..96d19552aa 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -235,13 +235,29 @@ and constants_of_modtype env mp modtype =
   | MTBfunsig _ -> []
 
 (* 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,_) -> con,None) constants in 
- Mod_subst.make_resolver resolve
-
+ 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_inline then
+              let constant = lookup_constant con' env in
+		if constant.Declarations.const_opaque then
+		  None
+		else
+		  option_map Declarations.force
+		    constant.Declarations.const_body
+	    else
+              None
+	  with Not_found -> error_no_such_label (con_label con')
+	in
+	  con,constr
+     ) constants
+ in
+   Mod_subst.make_resolver resolve
 
 let strengthen_const env mp l cb = 
   match cb.const_opaque, cb.const_body with