diff options
Diffstat (limited to 'backend')
-rw-r--r-- | backend/CMparser.mly | 11 | ||||
-rw-r--r-- | backend/CMtypecheck.ml | 1 | ||||
-rw-r--r-- | backend/Linearizeaux.ml | 3 | ||||
-rw-r--r-- | backend/RTLtypingaux.ml | 1 |
4 files changed, 6 insertions, 10 deletions
diff --git a/backend/CMparser.mly b/backend/CMparser.mly index f369f9ea..c83a46e5 100644 --- a/backend/CMparser.mly +++ b/backend/CMparser.mly @@ -15,7 +15,6 @@ %{ open Datatypes -open CList open Camlcoq open BinPos open BinInt @@ -313,9 +312,9 @@ let mkmatch expr cases = prog: global_declarations proc_list EOF - { { prog_funct = CList.rev $2; + { { prog_funct = List.rev $2; prog_main = intern_string "main"; - prog_vars = CList.rev $1; } } + prog_vars = List.rev $1; } } ; global_declarations: @@ -347,8 +346,8 @@ proc: temp_counter := 0; Coq_pair($1, Internal { fn_sig = $6; - fn_params = CList.rev $3; - fn_vars = CList.rev (CList.app tmp $9); + fn_params = List.rev $3; + fn_vars = List.rev (tmp @ $9); fn_stackspace = $8; fn_body = $10 }) } | EXTERN STRINGLIT COLON signature @@ -383,7 +382,7 @@ stack_declaration: var_declarations: /* empty */ { [] } - | var_declarations var_declaration { CList.app $2 $1 } + | var_declarations var_declaration { $2 @ $1 } ; var_declaration: diff --git a/backend/CMtypecheck.ml b/backend/CMtypecheck.ml index c4f45b22..819f269e 100644 --- a/backend/CMtypecheck.ml +++ b/backend/CMtypecheck.ml @@ -17,7 +17,6 @@ open Printf open Datatypes -open CList open Camlcoq open AST open Integers diff --git a/backend/Linearizeaux.ml b/backend/Linearizeaux.ml index d2d2f24a..3fdc56f2 100644 --- a/backend/Linearizeaux.ml +++ b/backend/Linearizeaux.ml @@ -15,7 +15,6 @@ open Coqlib open Datatypes open LTL open Lattice -open CList open Maps open Camlcoq @@ -81,4 +80,4 @@ let enumerate_aux f reach = emit_block (IntSet.remove npc pending) (pos_of_int npc) end in emit_block IntSet.empty f.fn_entrypoint; - CList.rev !enum + List.rev !enum diff --git a/backend/RTLtypingaux.ml b/backend/RTLtypingaux.ml index 632f2aa5..cc7edf49 100644 --- a/backend/RTLtypingaux.ml +++ b/backend/RTLtypingaux.ml @@ -13,7 +13,6 @@ (* Type inference for RTL *) open Datatypes -open CList open Camlcoq open Maps open AST |