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, 1 insertions, 1 deletions

diff --git a/kernel/entries.mli b/kernel/entries.mli
index 61c0b8c3bb..56ea852daf 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -61,7 +61,7 @@ type definition_entry = {
   const_entry_opaque : bool;
   const_entry_boxed  : bool }
 
-type parameter_entry = types
+type parameter_entry = types*bool  (*inline flag*)
 
 type constant_entry = 
   | DefinitionEntry of definition_entry