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
---
 kernel/mod_typing.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel/mod_typing.ml')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 5a3dade530..407ae73ca7 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -95,7 +95,7 @@ and check_with_aux_def env sign with_decl mp equiv =
 			let cb' = {cb with
 				     const_body = body;
 				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false false);
+                            (compile_constant_body env' body false);
                                      const_constraints = cst} in
 			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 		    | Some b ->
@@ -105,7 +105,7 @@ and check_with_aux_def env sign with_decl mp equiv =
 			let cb' = {cb with
 				     const_body = body;
 				     const_body_code = Cemitcodes.from_val
-                            (compile_constant_body env' body false false);
+                            (compile_constant_body env' body false);
                                      const_constraints = cst} in
 			  SEBstruct(before@((l,SFBconst(cb'))::after)),cb',cst
 	      end
-- 
cgit v1.2.3