From 77b71db8470553aed0476827ec2e39aed0cbb6ed Mon Sep 17 00:00:00 2001
From: letouzey
Date: Sun, 17 Jan 2010 13:31:10 +0000
Subject: Variant !F M for functor application that does not honor the Inline
 declarations

 For F(X:T), the application !F M works as F M, except that if module type T
 contains some "Inline" annotations, they are not taken in account when substituting
 X with M in F. See forthcoming commits for examples of use for this feature.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12678 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/vernacexpr.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index d95fdbec95..8e5f2d8fce 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -176,7 +176,7 @@ type inductive_expr =
 type one_inductive_expr =
   lident * local_binder list * constr_expr option * constructor_expr list
 
-type module_binder = bool option * lident list * module_ast
+type module_binder = bool option * lident list * module_ast_inl
 
 type grammar_tactic_prod_item_expr =
   | TacTerm of string
@@ -264,12 +264,12 @@ type vernac_expr =
 
   (* Modules and Module Types *)
   | VernacDeclareModule of bool option * lident *
-      module_binder list * module_ast
+      module_binder list * module_ast_inl
   | VernacDefineModule of bool option * lident *
-      module_binder list * module_ast module_signature * module_ast list
+      module_binder list * module_ast_inl module_signature * module_ast_inl list
   | VernacDeclareModuleType of lident *
-      module_binder list * module_ast list * module_ast list
-  | VernacInclude of module_ast list
+      module_binder list * module_ast_inl list * module_ast_inl list
+  | VernacInclude of module_ast_inl list
 
   (* Solving *)
 
-- 
cgit v1.2.3