source: extracted/fresh.mli @ 2716

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

...

File size: 1.2 KB
Line 
1open Preamble
2
3open CostLabel
4
5open Coqlib
6
7open Proper
8
9open PositiveMap
10
11open Deqsets
12
13open ErrorMessages
14
15open PreIdentifiers
16
17open Errors
18
19open Extralib
20
21open Setoids
22
23open Monad
24
25open Option
26
27open Lists
28
29open Positive
30
31open Identifiers
32
33open Arithmetic
34
35open Vector
36
37open Div_and_mod
38
39open Jmeq
40
41open Russell
42
43open List
44
45open Util
46
47open FoldStuff
48
49open BitVector
50
51open Extranat
52
53open Bool
54
55open Relations
56
57open Nat
58
59open Integers
60
61open Hints_declaration
62
63open Core_notation
64
65open Pts
66
67open Logic
68
69open Types
70
71open AST
72
73open Csyntax
74
75val max_id : AST.ident -> AST.ident -> AST.ident
76
77val max_id_of_env :
78  (AST.ident, Csyntax.type0) Types.prod List.list -> AST.ident
79
80val max_id_of_fn : Csyntax.function0 -> AST.ident
81
82val max_id_of_fundef : Csyntax.clight_fundef -> AST.ident
83
84val max_id_of_functs :
85  (AST.ident, Csyntax.clight_fundef) Types.prod List.list -> AST.ident
86
87val max_id_of_globvars :
88  ((AST.ident, AST.region) Types.prod, (AST.init_data List.list,
89  Csyntax.type0) Types.prod) Types.prod List.list -> AST.ident
90
91val max_id_of_program : Csyntax.clight_program -> AST.ident
92
93val universe_of_max : AST.ident -> Identifiers.universe
94
95val universe_for_program : Csyntax.clight_program -> Identifiers.universe
96
Note: See TracBrowser for help on using the repository browser.