diff options
author | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2009-07-04 13:28:38 +0200 |
commit | 3a420f4ad929e8372d32c735fd0fd89dfc0346a1 (patch) | |
tree | 943a01d103c1296dc7c07cb188af994354c4d9a3 /library/declare.ml | |
parent | 1769cbaddea77112dd6f336316d8eb9a0945a1e6 (diff) | |
parent | e4282ea99c664d8d58067bee199cbbcf881b60d5 (diff) |
Merge commit 'upstream/8.2.pl1+dfsg'
Diffstat (limited to 'library/declare.ml')
-rw-r--r-- | library/declare.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/library/declare.ml b/library/declare.ml index 4bdc11c3..c349bef1 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: declare.ml 11282 2008-07-28 11:51:53Z msozeau $ *) +(* $Id: declare.ml 12187 2009-06-13 19:36:59Z msozeau $ *) (** This module is about the low-level declaration of logical objects *) @@ -43,7 +43,7 @@ let set_xml_declare_inductive f = xml_declare_inductive := if_xml f type section_variable_entry = | SectionLocalDef of constr * types option * bool (* opacity *) - | SectionLocalAssum of types * bool * bool (* Implicit status, Keep *) + | SectionLocalAssum of types * bool * identifier list (* Implicit status, Keep *) type variable_declaration = dir_path * section_variable_entry * logical_kind @@ -58,7 +58,7 @@ let cache_variable ((sp,_),o) = | SectionLocalAssum (ty, impl, keep) -> let cst = Global.push_named_assum (id,ty) in let impl = if impl then Lib.Implicit else Lib.Explicit in - let keep = if keep then Some ty else None in + let keep = if keep <> [] then Some (ty, keep) else None in impl, true, cst, keep | SectionLocalDef (c,t,opaq) -> let cst = Global.push_named_def (id,c,t) in |