From 4ee0cedff7726a56ebd53125995a7ae131660b4a Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 18 Aug 2020 13:07:54 +0200
Subject: Rename VM-related kernel/cfoo files to kernel/vmfoo

---
 kernel/cbytecodes.mli | 78 ---------------------------------------------------
 1 file changed, 78 deletions(-)
 delete mode 100644 kernel/cbytecodes.mli

(limited to 'kernel/cbytecodes.mli')

diff --git a/kernel/cbytecodes.mli b/kernel/cbytecodes.mli
deleted file mode 100644
index b703058fb7..0000000000
--- a/kernel/cbytecodes.mli
+++ /dev/null
@@ -1,78 +0,0 @@
-(************************************************************************)
-(*         *   The Coq Proof Assistant / The Coq Development Team       *)
-(*  v      *         Copyright INRIA, CNRS and contributors             *)
-(* <O___,, * (see version control and CREDITS file for authors & dates) *)
-(*   \VV/  **************************************************************)
-(*    //   *    This file is distributed under the terms of the         *)
-(*         *     GNU Lesser General Public License Version 2.1          *)
-(*         *     (see LICENSE file for the text of the license)         *)
-(************************************************************************)
-
-(* $Id$ *)
-
-open Names
-open Vmvalues
-open Constr
-
-module Label :
-  sig
-    type t = int
-    val no : t
-    val create : unit -> t
-    val reset_label_counter : unit -> unit
-  end
-
-type instruction =
-  | Klabel of Label.t
-  | Kacc of int                         (** accu = sp[n] *)
-  | Kenvacc of int                      (** accu = coq_env[n] *)
-  | Koffsetclosure of int               (** accu = &coq_env[n] *)
-  | Kpush                               (** sp = accu :: sp *)
-  | Kpop of int                         (** sp = skipn n sp *)
-  | Kpush_retaddr of Label.t            (** sp = pc :: coq_env :: coq_extra_args :: sp ; coq_extra_args = 0 *)
-  | Kapply of int                       (** number of arguments (arguments on top of stack) *)
-  | Kappterm of int * int               (** number of arguments, slot size *)
-  | Kreturn of int                      (** slot size *)
-  | Kjump
-  | Krestart
-  | Kgrab of int                        (** number of arguments *)
-  | Kgrabrec of int                     (** rec arg *)
-  | Kclosure of Label.t * int           (** label, number of free variables *)
-  | Kclosurerec of int * int * Label.t array * Label.t array
-                   (** nb fv, init, lbl types, lbl bodies *)
-  | Kclosurecofix of int * int * Label.t array * Label.t array
-                   (** nb fv, init, lbl types, lbl bodies *)
-  | Kgetglobal of Constant.t
-  | Kconst of structured_constant
-  | Kmakeblock of (* size: *) int * tag (** allocate an ocaml block. Index 0
-                                         ** is accu, all others are popped from
-                                         ** the top of the stack  *)
-  | Kmakeprod
-  | Kmakeswitchblock of Label.t * Label.t * annot_switch * int
-  | Kswitch of Label.t array * Label.t array (** consts,blocks *)
-  | Kpushfields of int
-  | Kfield of int                       (** accu = accu[n] *)
-  | Ksetfield of int                    (** accu[n] = sp[0] ; sp = pop sp *)
-  | Kstop
-  | Ksequence of bytecodes * bytecodes
-  | Kproj of Projection.Repr.t
-  | Kensurestackcapacity of int
-
-  | Kbranch of Label.t                  (** jump to label, is it needed ? *)
-  | Kprim of CPrimitives.t * pconstant option
-  | Kcamlprim of CPrimitives.t * Label.t
-  | Kareint of int
-
-and bytecodes = instruction list
-
-val pp_bytecodes : bytecodes -> Pp.t
-
-type fv_elem =
-  FVnamed of Id.t
-| FVrel of int
-| FVuniv_var of int
-| FVevar of Evar.t
-
-type fv = fv_elem array
-
-val pp_fv_elem : fv_elem -> Pp.t
-- 
cgit v1.2.3