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
---
 library/declare.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'library')

diff --git a/library/declare.ml b/library/declare.ml
index f729f133db..6e9835487b 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -177,7 +177,7 @@ let discharge_constant ((sp,kn),(cdt,dhyps,kind)) =
   Some (GlobalRecipe recipe,(discharged_hyps kn sechyps)@dhyps,kind)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
-let dummy_constant_entry = ConstantEntry (ParameterEntry mkProp)
+let dummy_constant_entry = ConstantEntry (ParameterEntry (mkProp,false))
 
 let dummy_constant (ce,_,mk) = dummy_constant_entry,[],mk
 
-- 
cgit v1.2.3