From f19a9d9d3a410fda982b2cf9154da5774f9ec84f Mon Sep 17 00:00:00 2001 From: letouzey Date: Fri, 28 Jan 2011 13:20:41 +0000 Subject: 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 --- tactics/leminv.ml | 3 +-- tactics/rewrite.ml4 | 3 +-- 2 files changed, 2 insertions(+), 4 deletions(-) (limited to 'tactics') diff --git a/tactics/leminv.ml b/tactics/leminv.ml index c31980158..95814302d 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -236,8 +236,7 @@ let add_inversion_lemma name env sigma t sort dep inv_op = (DefinitionEntry { const_entry_body = invProof; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = true && (Flags.boxed_definitions())}, + const_entry_opaque = false }, IsProof Lemma) in () diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 188bc3dc5..a6a36672b 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -1345,8 +1345,7 @@ let declare_projection n instance_id r = let cst = { const_entry_body = term; const_entry_type = Some typ; - const_entry_opaque = false; - const_entry_boxed = false } + const_entry_opaque = false } in ignore(Declare.declare_constant n (Entries.DefinitionEntry cst, Decl_kinds.IsDefinition Decl_kinds.Definition)) -- cgit v1.2.3