A  
abstract [Sum]  
answer [Sig]  
atom [Enumsolver_types]  
atom [Solver_types]  
C  
clause [Enumsolver_types]  
clause [Solver_types]  
color [Util]  
combinator [Smt.Formula] 
The type of operators

comparator [Smt.Formula] 
The type of comparators:

const [Types] 
constant: it can be an integer, a real or a constant name

D  
dnf [Ast] 
Disjunctive normal form: each element of the list is a disjunct

E  
elem [Heap.S]  
elt [Use.ST]  
elt [Use]  
elt [Literal.S]  
error [Smt]  
error [Typing]  
exp [Explanation]  
G  
glob_update [Ast]  
H  
hash_consed [Hashcons]  
I  
ident [Enumsolver_types]  
input [Sig]  
inst_trans [Forward] 
the type of instantiated transitions

K  
key [Hashcons.S_consed]  
kind [Ast] 
the kind of nodes

L  
literal [Sig]  
loc [Util] 
Location in file

N  
name_kind [Symbols]  
node_cube [Ast] 
the type of nodes, i.e.

O  
op_comp [Types] 
comparison operators for litterals

operator [Symbols]  
operator [Smt.Term] 
The type of operators

P  
possible_result [Forward]  
premise [Enumsolver_types]  
premise [Solver_types]  
R  
r [Sig.C]  
r [Sig.X]  
r [Sig.COMBINATOR]  
r [Polynome.S]  
r [Sig.RELATION]  
r [Sig.THEORY] 
Type of representants of terms of the theory

r [Polynome.T]  
reason [Enumsolver_types]  
reason [Solver_types]  
result [Sig]  
result [Bwd]  
S  
sort [Types] 
sort of single symbol

state [Enumsolver.Make]  
state [Solver.Make]  
state [Smt.Solver] 
The type of the internal state of the solver (see
Smt.Solver.save_state and
Smt.Solver.restore_state ).

subst [Variable] 
the type of variable substitutions

swts [Ast] 
The type of case switches case  c1 : t1  c2 : t2  _ : tn

system [Ast] 
type of untyped transition systems constructed by parsing

T  
t [Use.Make]  
t [Use.ST]  
t [Use.S]  
t [Use.T]  
t [Uf.S]  
t [Ty]  
t [Term]  
t [Symbols]  
t [Smt.Formula] 
The type of ground formulas

t [Smt.Term] 
The type of terms

t [Smt.Symbol] 
The type of function symbols

t [Smt.Type] 
The type of types in AltErgo light

t [Sig.C]  
t [Literal.OrderedType]  
t [Literal.S]  
t [Intervals]  
t [Explanation]  
t [Cc.S]  
t [Sig.RELATION]  
t [Sig.THEORY] 
Type of terms of the theory

t [Polynome.T]  
t [Bitv]  
t [Vec]  
t [Iheap]  
t [Hstring] 
The type of Hashconsed string

t [Heap.OrderType]  
t [Heap.S]  
t [Hashcons.HashedType_consed]  
t [Hashcons.HashedType]  
t [Hashcons.S]  
t [Variable] 
the type of variables

t [Types.ArrayAtom] 
values of this type should be constructed with the invariant that the
array must be sorted at all times

t [Types.Atom] 
the type of atoms

t [Types.Term]  
t [Node] 
the type of nodes constructed during the search

t [Cubetrie] 
Trie, mapping sets of atoms (i.e.

t [Cube] 
the type of cubes, i.e.

t [Bwd.PriorityNodeQueue]  
t_system [Ast] 
type of typed transition systems

term [Types] 
the type of terms

th [Sig.COMBINATOR]  
trace [Options]  
trace [Ast] 
type of error traces, also the type of history of nodes

trace_step [Ast] 
type of elementary steps of error traces

transition [Ast] 
type of parameterized transitions with function

transition_func [Ast] 
functionnal form, computed during typing phase

transition_info [Ast] 
type of parameterized transitions

type_constructors [Ast] 
Type and constructors declaration:
("t", ["A";"B"]) represents the
declaration of type t with two constructors A and B .

U  
update [Ast] 
conditionnal updates with cases, ex.

V  
var [Enumsolver_types]  
var [Solver_types]  
view [Term]  
view [Literal]  
viz_prog [Options] 