diff options
| author | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-29 09:13:53 +0000 |
|---|---|---|
| committer | xleroy <xleroy@fca1b0fc-160b-0410-b1d3-a4f43f01ea2e> | 2009-01-29 09:13:53 +0000 |
| commit | 26fcc4dbd92f367ecb20f4457cdf887eea0b6568 (patch) | |
| tree | 0bec42a8bbb4c8d70e31d60e055409ef31e10da3 /backend | |
| parent | f6ecbb948ccf7f8a4e156eb29e3a41e7f2953407 (diff) | |
| download | compcert-26fcc4dbd92f367ecb20f4457cdf887eea0b6568.tar.gz compcert-26fcc4dbd92f367ecb20f4457cdf887eea0b6568.zip | |
Conflict between extraction/CList and cil/obj/xxx/clist on case-insensitive file systems. Replaced CList by CoqList and likewise for CString and CInt. Removed useless references to CList in hand-written Caml code.
git-svn-id: https://yquem.inria.fr/compcert/svn/compcert/trunk@951 fca1b0fc-160b-0410-b1d3-a4f43f01ea2e
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 |