source: extracted/statusProofs.ml @ 2601

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

Extraction to ocaml is now working, with a couple of bugs left.
One limitation is that it is not possible to have two files with the
same name in different directories. Therefore this commit renames files
to avoid this situation.

The extracted directory contains:

  1. a snapshot of the .ml(i) files extracted from CerCo? by running ocamlc.opt -extract_ocaml compiler.ma The files have been patched by hand to implement all strings and fix the bugs.
  2. a file PROBLEMS that describes the remaining problems, i.e. bugs and axioms to be implemented

To obtain the compiler, run ocamlbuild compiler.byte.
At the moment it fails because of the three remaining axioms.

File size: 606 bytes
Line 
1open Preamble
2
3open BitVectorTrie
4
5open LabelledObjects
6
7open Coqlib
8
9open Floats
10
11open Arithmetic
12
13open Integers
14
15open AST
16
17open CostLabel
18
19open Proper
20
21open PositiveMap
22
23open Deqsets
24
25open PreIdentifiers
26
27open Errors
28
29open Extralib
30
31open Setoids
32
33open Monad
34
35open Option
36
37open Lists
38
39open Positive
40
41open Identifiers
42
43open Char
44
45open String
46
47open Extranat
48
49open Vector
50
51open Div_and_mod
52
53open Jmeq
54
55open Russell
56
57open Types
58
59open List
60
61open Util
62
63open FoldStuff
64
65open Bool
66
67open Hints_declaration
68
69open Core_notation
70
71open Pts
72
73open Logic
74
75open Relations
76
77open Nat
78
79open BitVector
80
81open ASM
82
83open Status
84
Note: See TracBrowser for help on using the repository browser.