source: extracted/policyStep.mli @ 2773

Last change on this file since 2773 was 2773, checked in by sacerdot, 7 years ago
  1. everything extracted again after all bugs in Matita's extraction have been fixed. No more need for manual patching
  2. new extraction after file reorganization (by James)
File size: 864 bytes
RevLine 
[2717]1open Preamble
2
3open Assembly
4
5open Status
6
7open Fetch
8
[2773]9open BitVectorTrie
10
[2717]11open String
12
13open Exp
14
15open Arithmetic
16
[2773]17open Vector
18
19open FoldStuff
20
21open BitVector
22
23open Extranat
24
[2717]25open Integers
26
27open AST
28
[2773]29open LabelledObjects
[2717]30
31open Proper
32
33open PositiveMap
34
35open Deqsets
36
37open ErrorMessages
38
39open PreIdentifiers
40
41open Errors
42
43open Extralib
44
45open Setoids
46
47open Monad
48
49open Option
50
51open Div_and_mod
52
53open Jmeq
54
55open Russell
56
[2773]57open Util
[2717]58
59open List
60
[2773]61open Lists
[2717]62
63open Bool
64
[2773]65open Relations
66
67open Nat
68
69open Positive
70
[2717]71open Hints_declaration
72
73open Core_notation
74
75open Pts
76
77open Logic
78
[2773]79open Types
[2717]80
[2773]81open Identifiers
[2717]82
[2773]83open CostLabel
[2717]84
85open ASM
86
87open PolicyFront
88
89val jump_expansion_step :
90  ASM.labelled_instruction List.list Types.sig0 -> Fetch.label_map Types.sig0
91  -> PolicyFront.ppc_pc_map Types.sig0 -> (Bool.bool, PolicyFront.ppc_pc_map
92  Types.option) Types.prod Types.sig0
93
Note: See TracBrowser for help on using the repository browser.