Context Navigation

source: extracted/lIN.ml @ 2746

Last change on this file since 2746 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: 894 bytes

Line
1	open Preamble
2
3	open String
4
5	open Sets
6
7	open Listb
8
9	open LabelledObjects
10
11	open Graphs
12
13	open I8051
14
15	open Order
16
17	open Registers
18
19	open BitVectorTrie
20
21	open CostLabel
22
23	open Hide
24
25	open Proper
26
27	open PositiveMap
28
29	open Deqsets
30
31	open ErrorMessages
32
33	open PreIdentifiers
34
35	open Errors
36
37	open Extralib
38
39	open Setoids
40
41	open Monad
42
43	open Option
44
45	open Lists
46
47	open Identifiers
48
49	open Integers
50
51	open AST
52
53	open Division
54
55	open Exp
56
57	open Arithmetic
58
59	open Extranat
60
61	open Vector
62
63	open Div_and_mod
64
65	open Jmeq
66
67	open Russell
68
69	open List
70
71	open Util
72
73	open FoldStuff
74
75	open BitVector
76
77	open Types
78
79	open Bool
80
81	open Relations
82
83	open Nat
84
85	open Hints_declaration
86
87	open Core_notation
88
89	open Pts
90
91	open Logic
92
93	open Positive
94
95	open Z
96
97	open BitVectorZ
98
99	open Pointers
100
101	open ByteValues
102
103	open BackEndOps
104
105	open Joint
106
107	open Joint_LTL_LIN
108
109	( val lIN : Joint.lin_params )
110	let lIN =
111	Joint_LTL_LIN.lTL_LIN
112
113	type lin_program = Joint.joint_program
114

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