diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-01-12 16:02:20 +0100 |
| commit | 97fefe1fcca363a1317e066e7f4b99b9c1e9987b (patch) | |
| tree | 97ec6b7d831cc5fb66328b0c63a11db1cbb2f158 /kernel/cemitcodes.ml | |
| parent | 300293c119981054c95182a90c829058530a6b6f (diff) | |
Imported Upstream version 8.4~betaupstream/8.4_beta
Diffstat (limited to 'kernel/cemitcodes.ml')
| -rw-r--r-- | kernel/cemitcodes.ml | 21 |
1 files changed, 14 insertions, 7 deletions
diff --git a/kernel/cemitcodes.ml b/kernel/cemitcodes.ml index 0b4df194..1f00a70e 100644 --- a/kernel/cemitcodes.ml +++ b/kernel/cemitcodes.ml @@ -1,3 +1,15 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* Author: Benjamin Grégoire as part of the bytecode-based virtual reduction + machine, Oct 2004 *) +(* Extension: Arnaud Spiwack (support for native arithmetic), May 2005 *) + open Names open Term open Cbytecodes @@ -321,12 +333,12 @@ let subst_to_patch s (code,pl,fv) = code,List.rev_map (subst_patch s) pl,fv type body_code = - | BCdefined of bool * to_patch + | BCdefined of to_patch | BCallias of constant | BCconstant let subst_body_code s = function - | BCdefined (b,tp) -> BCdefined (b,subst_to_patch s tp) + | BCdefined tp -> BCdefined (subst_to_patch s tp) | BCallias kn -> BCallias (fst (subst_con s kn)) | BCconstant -> BCconstant @@ -338,11 +350,6 @@ let force = force subst_body_code let subst_to_patch_subst = subst_substituted -let is_boxed tps = - match force tps with - | BCdefined(b,_) -> b - | _ -> false - let repr_body_code = repr_substituted let to_memory (init_code, fun_code, fv) = |