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, 4 insertions, 2 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index d0f2289dc4..1be251a503 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -49,7 +49,8 @@ type constant_body = {
     const_body_code : Cemitcodes.to_patch_substituted;
    (* const_type_code : Cemitcodes.to_patch; *)
     const_constraints : constraints;
-    const_opaque : bool }
+    const_opaque : bool; 
+    const_inline : bool}
 
 (*s Inductive types (internal representation with redundant
     information). *)
@@ -202,7 +203,8 @@ let subst_const_body sub cb = {
     const_body_code = Cemitcodes.subst_to_patch_subst sub cb.const_body_code;
     (*const_type_code = Cemitcodes.subst_to_patch sub cb.const_type_code;*)
     const_constraints = cb.const_constraints;
-    const_opaque = cb.const_opaque } 
+    const_opaque = cb.const_opaque;
+    const_inline = cb.const_inline} 
 
 let subst_arity sub = function
 | Monomorphic s ->