From 40425048feff138e6c67555c7ee94142452d1cae Mon Sep 17 00:00:00 2001
From: soubiran
Date: Wed, 25 Apr 2007 15:13:45 +0000
Subject: 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
---
 kernel/declarations.mli | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/declarations.mli')

diff --git a/kernel/declarations.mli b/kernel/declarations.mli
index 22cfd62a0c..7f7f7dcc39 100644
--- a/kernel/declarations.mli
+++ b/kernel/declarations.mli
@@ -47,7 +47,8 @@ type constant_body = {
     const_body_code : to_patch_substituted;
    (*i const_type_code : to_patch;i*)
     const_constraints : constraints;
-    const_opaque : bool }
+    const_opaque : bool;
+    const_inline : bool}
 
 val subst_const_body : substitution -> constant_body -> constant_body
 
-- 
cgit v1.2.3