source: extracted/registers.ml @ 2602

Last change on this file since 2602 was 2602, checked in by piccolo, 7 years ago

Dead code commented out.

File size: 745 bytes
Line 
1open Preamble
2
3open Proper
4
5open PositiveMap
6
7open Deqsets
8
9open PreIdentifiers
10
11open Errors
12
13open Extralib
14
15open Setoids
16
17open Monad
18
19open Option
20
21open Div_and_mod
22
23open Jmeq
24
25open Russell
26
27open Util
28
29open Lists
30
31open Positive
32
33open Char
34
35open Bool
36
37open Relations
38
39open Nat
40
41open List
42
43open String
44
45open Hints_declaration
46
47open Core_notation
48
49open Pts
50
51open Logic
52
53open Types
54
55open Identifiers
56
57open Order
58
59(** val registerTag : String.string **)
60let registerTag = "register tag"
61  (*failwith "AXIOM TO BE REALIZED"*)
62
63type register = PreIdentifiers.identifier
64
65(** val register_eq : register -> register -> (__, __) Types.sum **)
66let register_eq =
67  Identifiers.identifier_eq registerTag
68
69type 'a register_env = 'a Identifiers.identifier_map
Note: See TracBrowser for help on using the repository browser.