source: extracted/cexecSound.ml @ 2731

Last change on this file since 2731 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
RevLine 
[2601]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
[2717]29open BitVectorTrie
30
[2601]31open CostLabel
32
33open PositiveMap
34
35open Deqsets
36
37open Lists
38
39open Identifiers
40
41open Integers
42
43open AST
44
45open Division
46
[2717]47open Exp
48
[2601]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
[2649]73open ErrorMessages
74
[2601]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.