Index of values


(>>) [Search_monad]	bind and return
(>>\|) [Search_monad]	non-deterministic choice
A
aac_normalise [Aac_rewrite]
aac_reflexivity [Aac_rewrite]
aac_rewrite [Aac_rewrite]
add [Theory.Sigma]	`add ty n x map` adds the value `x` of type `ty` with key `n` in `map`
add [Aac_rewrite]
add_symbol [Theory.Trans]	`add_symbol` adds a given binary symbol to the environment of known stuff.
anomaly [Coq]
B
build [Coq.Rewrite]	build the constr to rewrite, with lambda abstractions
C
choose [Search_monad]
count [Search_monad]
cps_mk_letin [Coq]	`cps_mk_letin name v` binds the constr `v` using a letin tactic
cps_resolve_one_typeclass [Coq]
D
debug [Helper.CONTROL]
debug [Helper.Debug]	`debug` prints the string and end it with a newline
debug_exception [Helper.Debug]
decide_thm [Theory.Stubs]	The main lemma of our theory, that is `compare (norm u) (norm v) = Eq -> eval u == eval v`
decomp_term [Coq]
E
empty [Theory.Sigma]	`empty ty` create an empty map of type `ty`
empty_envs [Theory.Trans]
equal_aac [Matcher.Terms]	Test for equality of terms modulo AACU (relies on the following canonical representation of terms).
eval [Theory.Stubs]	The evaluation fonction, used to convert a reified coq term to a raw coq term
evar_binary [Coq]
evar_relation [Coq]
F
fail [Search_monad]	failure
filter [Search_monad]
find_global [Coq]
fold [Search_monad]	folding through the collection
from_relation [Coq.Equivalence]
G
get_efresh [Coq]
get_fresh [Coq]
get_hypinfo [Coq.Rewrite]	`get_hypinfo H ?check_type l2r` analyse the hypothesis H, and build the related hypinfo.
I
infer [Coq.Equivalence]
instantiate [Matcher.Subst]
ir_of_envs [Theory.Trans]
ir_to_units [Theory.Trans]
is_empty [Search_monad]
L
lift [Theory.Stubs]
lift_normalise_thm [Theory.Stubs]
lift_proj_equivalence [Theory.Stubs]
lift_reflexivity [Theory.Stubs]
lift_transitivity_left [Theory.Stubs]
lift_transitivity_right [Theory.Stubs]
linear [Matcher]	`linear` expands a multiset into a simple list
M
make [Coq.Equivalence]
make [Coq.Relation]
match_as_equation [Coq]	`match_as_equation ?context env sigma c` try to decompose c as a relation applied to two terms.
matcher [Matcher]	`matcher p t` computes the set of solutions to the given top-level matching problem (`p` is the pattern, `t` is the term).
mk_equivalence [Coq.Classes]
mk_letin [Coq]
mk_morphism [Coq.Classes]
mk_mset [Theory]
mk_pack [Theory.Sym]	`mk_pack rlt (ar,value,morph)`
mk_reflexive [Coq.Classes]
mk_reifier [Theory.Trans]
mk_transitive [Coq.Classes]
N
nf_equal [Matcher.Terms]
nf_evar [Coq]
nf_term_compare [Matcher.Terms]
none [Coq.Option]
null [Theory.Sym]	`null` builds a dummy (identity) symbol, given an `Coq.Relation.t`
O
of_int [Coq.Nat]
of_int [Coq.Pos]
of_list [Theory.Sigma]	`of_list ty null l` translates an OCaml association list into a Coq one
of_list [Coq.List]	`of_list ty l`
of_option [Coq.Option]
of_pair [Coq.Pair]
P
pair [Coq.Pair]
pr_aac_args [Aac_rewrite]
pr_constr [Helper.Debug]	`pr_constr` print a Coq constructor, that can be labelled by a string
print [Print]	The main printing function.
printing [Helper.CONTROL]
R
raw_constr_of_t [Theory.Trans]	`raw_constr_of_t` rebuilds a term in the raw representation, and reconstruct the named products on top of it.
reif_constr_of_t [Theory.Trans]	`reif_constr_of_t reifier t` rebuilds the term `t` in the reified form.
resolve_one_typeclass [Coq]
return [Search_monad]
retype [Coq]
rewrite [Coq.Rewrite]	`rewrite ?abort hypinfo subst` builds the rewriting tactic associated with the given `subst` and `hypinfo`.
S
show_proof [Coq]	print the current proof term
some [Coq.Option]
sort [Search_monad]
split [Coq.Equivalence]
split [Coq.Relation]
sprint [Search_monad]
sprint [Matcher.Subst]
sprint_nf_term [Matcher.Terms]
subterm [Matcher]	`subterm p t` computes a set of solutions to the given subterm-matching problem.
T
t_of_constr [Theory.Trans]
t_of_term [Matcher.Terms]
tclDEBUG [Coq]	emit debug messages to see which tactics are failing
tclPRINT [Coq]	print the current goal
tclRETYPE [Coq]
tclTIME [Coq]	time the execution of a tactic
term_of_t [Matcher.Terms]	we have the following property: `a` and `b` are equal modulo AACU iif `nf_equal (term_of_t a) (term_of_t b) = true`
time [Helper.CONTROL]
time [Helper.Debug]	`time` computes the time spent in a function, and then print it using the given format
to_fun [Theory.Sigma]	`to_fun ty null map` converts a Coq association list into a Coq function (with default value `null`)
to_list [Search_monad]
to_list [Matcher.Subst]
to_relation [Coq.Equivalence]
typ [Theory.Sym]
typ [Coq.Nat]
typ [Coq.Pos]
typ [Coq.Option]
typ [Coq.Pair]
type_of_list [Coq.List]	`type_of_list ty`
U
user_error [Coq]
W
warning [Coq]