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