refactor(library/unifier): group flex_rigid case related methods in a functional object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(library/unifier): improve flex_rigid performance

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/converter): missing delay_check case

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
perf(kernel/abstract): improve mk_binding performance

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/unifier): remove redundant code

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(kernel/environment): initialization problem on OSX

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(util/script_state): weird crash with Lua 5.1

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library): add definitions_cache datastructure for implementing .clean files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
chore(shell/lean): rename shortname for --luahook option

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add option --cache

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
refactor(library/tactic/expr_to_tactic): use annotations for implementing 'by'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/Makefile.common): use new --cache/-c option at Makefile.common

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): add 'INSERT' and 'REMOVE' commands to lean 'server', make sure all commands use the same convention for numbering lines, update server.org

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean/server): use definitions_cache in the server object

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add classes for relations
feat(library/hott): begin porting Coq HoTT
feat(library/hott): add theorems about paths
feat(library/hott/path_groupoids): add more theorems
refactor(library/hott/path_groupoids): clean up hard examples