diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-28 13:20:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-01-28 13:20:41 +0000 |
| commit | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (patch) | |
| tree | 23e166d4564ec1382afb60ec0d03e976dcaff377 /library | |
| parent | c7fb97fd915a732e1d91ca59fd635c95235052ce (diff) | |
Remove the "Boxed" syntaxes and the const_entry_boxed field
According to B. Gregoire, this stuff is obsolete. Fine control
on when to launch the VM in conversion problems is now provided
by VMcast. We were already almost never boxing definitions anymore
in stdlib files.
"(Un)Boxed Definition foo" will now trigger a parsing error,
same with Fixpoint. The option "(Un)Set Boxed Definitions"
aren't there anymore, but tolerated (as no-ops), since unknown
options raise a warning instead of an error by default.
Some more cleaning could be done in the vm.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13806 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/decl_kinds.ml | 10 | ||||
| -rw-r--r-- | library/decl_kinds.mli | 6 | ||||
| -rw-r--r-- | library/declare.ml | 3 |
3 files changed, 7 insertions, 12 deletions
diff --git a/library/decl_kinds.ml b/library/decl_kinds.ml index 5ae048d65..ba40f98c0 100644 --- a/library/decl_kinds.ml +++ b/library/decl_kinds.ml @@ -15,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (* Kinds used in proofs *) @@ -84,12 +82,12 @@ let string_of_theorem_kind = function | Proposition -> "Proposition" | Corollary -> "Corollary" -let string_of_definition_kind (l,boxed,d) = - match (l,d) with +let string_of_definition_kind def = + match def with | Local, Coercion -> "Coercion Local" | Global, Coercion -> "Coercion" | Local, Definition -> "Let" - | Global, Definition -> if boxed then "Boxed Definition" else "Definition" + | Global, Definition -> "Definition" | Local, SubClass -> "Local SubClass" | Global, SubClass -> "SubClass" | Global, CanonicalStructure -> "Canonical Structure" diff --git a/library/decl_kinds.mli b/library/decl_kinds.mli index 6b03442f5..88ef763c9 100644 --- a/library/decl_kinds.mli +++ b/library/decl_kinds.mli @@ -15,8 +15,6 @@ type locality = | Local | Global -type boxed_flag = bool - type theorem_kind = | Theorem | Lemma @@ -52,7 +50,7 @@ type assumption_object_kind = Definitional | Logical | Conjectural *) type assumption_kind = locality * assumption_object_kind -type definition_kind = locality * boxed_flag * definition_object_kind +type definition_kind = locality * definition_object_kind (** Kinds used in proofs *) @@ -74,7 +72,7 @@ type logical_kind = val logical_kind_of_goal_kind : goal_object_kind -> logical_kind val string_of_theorem_kind : theorem_kind -> string val string_of_definition_kind : - locality * boxed_flag * definition_object_kind -> string + locality * definition_object_kind -> string (** About locality *) diff --git a/library/declare.ml b/library/declare.ml index a9c463020..fa95fe313 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -160,8 +160,7 @@ let hcons_constant_declaration = function DefinitionEntry { const_entry_body = hcons1_constr ce.const_entry_body; const_entry_type = Option.map hcons1_constr ce.const_entry_type; - const_entry_opaque = ce.const_entry_opaque; - const_entry_boxed = ce.const_entry_boxed } + const_entry_opaque = ce.const_entry_opaque } | cd -> cd let declare_constant_common id dhyps (cd,kind) = |