diff options
| author | letouzey | 2011-01-28 13:20:41 +0000 |
|---|---|---|
| committer | letouzey | 2011-01-28 13:20:41 +0000 |
| commit | f19a9d9d3a410fda982b2cf9154da5774f9ec84f (patch) | |
| tree | 23e166d4564ec1382afb60ec0d03e976dcaff377 /toplevel/autoinstance.ml | |
| 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 'toplevel/autoinstance.ml')
| -rw-r--r-- | toplevel/autoinstance.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/toplevel/autoinstance.ml b/toplevel/autoinstance.ml index 4c2353fc88..242a8e52b4 100644 --- a/toplevel/autoinstance.ml +++ b/toplevel/autoinstance.ml @@ -179,8 +179,9 @@ let declare_record_instance gr ctx params = let ident = make_instance_ident gr in let def = it_mkLambda_or_LetIn (applistc (constr_of_global gr) params) ctx in let def = deep_refresh_universes def in - let ce = { const_entry_body=def; const_entry_type=None; - const_entry_opaque=false; const_entry_boxed=false } in + let ce = { const_entry_body=def; + const_entry_type=None; + const_entry_opaque=false } in let cst = Declare.declare_constant ident (DefinitionEntry ce,Decl_kinds.IsDefinition Decl_kinds.StructureComponent) in new_instance_message ident (Typeops.type_of_constant (Global.env()) cst) def @@ -193,8 +194,9 @@ let declare_class_instance gr ctx params = let def = deep_refresh_universes def in let typ = deep_refresh_universes typ in let ce = Entries.DefinitionEntry - { const_entry_type=Some typ; const_entry_body=def; - const_entry_opaque=false; const_entry_boxed=false } in + { const_entry_type=Some typ; + const_entry_body=def; + const_entry_opaque=false } in try let cst = Declare.declare_constant ident (ce,Decl_kinds.IsDefinition Decl_kinds.Instance) in |