Leonardo de Moura 3b38f71f11 fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type ... We had to change subtype to use Sort since the axiom strong_indefinite_description uses it. see #1341		2017-01-30 11:54:00 -08:00
..
lean	fix(library,tests/lean): fix run/interactive tests, and problems in the standard library due to the new interpretation for Type	2017-01-30 11:54:00 -08:00
smt2	feat(library/tactic): store name of current declaration in tactic_state	2017-01-28 08:27:19 +01:00