Context Navigation

source: extracted/cexecSound.ml @ 2717

Last change on this file since 2717 was 2717, checked in by sacerdot, 7 years ago

Extracted code for the whole compiler.
The space cost model is not there yet.

I have fixed by hand the few extraction problems
(i.e. composed coercions not extracted and type
definitions with wrong syntax).

I have also changed all axioms to be implemented
so that they do not fail at initialization time.

File size: 895 bytes

Line
1	open Preamble
2
3	open TypeComparison
4
5	open ClassifyOp
6
7	open Smallstep
8
9	open Csyntax
10
11	open Extra_bool
12
13	open FrontEndVal
14
15	open Hide
16
17	open ByteValues
18
19	open GenMem
20
21	open FrontEndMem
22
23	open Globalenvs
24
25	open Csem
26
27	open SmallstepExec
28
29	open BitVectorTrie
30
31	open CostLabel
32
33	open PositiveMap
34
35	open Deqsets
36
37	open Lists
38
39	open Identifiers
40
41	open Integers
42
43	open AST
44
45	open Division
46
47	open Exp
48
49	open Arithmetic
50
51	open Extranat
52
53	open Vector
54
55	open FoldStuff
56
57	open BitVector
58
59	open Z
60
61	open BitVectorZ
62
63	open Pointers
64
65	open Coqlib
66
67	open Values
68
69	open Events
70
71	open Proper
72
73	open ErrorMessages
74
75	open Option
76
77	open Setoids
78
79	open Monad
80
81	open Positive
82
83	open PreIdentifiers
84
85	open Errors
86
87	open IOMonad
88
89	open IO
90
91	open Div_and_mod
92
93	open Jmeq
94
95	open Russell
96
97	open Util
98
99	open Bool
100
101	open Relations
102
103	open Nat
104
105	open List
106
107	open Hints_declaration
108
109	open Core_notation
110
111	open Pts
112
113	open Logic
114
115	open Types
116
117	open Extralib
118
119	open Cexec
120
121	open CexecInd
122

Note: See TracBrowser for help on using the repository browser.

Download in other formats: