matita.cs.unibo.it Git - fireball-separation.git/history

]> matita.cs.unibo.it Git - fireball-separation.git/history - ocaml/simple.ml

projects / fireball-separation.git / history

[fireball-separation.git] / ocaml / simple.ml

2018-06-11	acondolu	Fix: it was always stepping on one non-existing argument	blob \| commitdiff \| raw
2018-06-10	acondolu	(Almost-)Correct handling of garbage in Simple	blob \| commitdiff \| raw \| diff to current
2018-06-10	acondolu	Using C instead of @ to combine more convergents in...	blob \| commitdiff \| raw \| diff to current
2018-06-10	acondolu	Improved definition of eta_eq	blob \| commitdiff \| raw \| diff to current
2018-06-10	acondolu	Step possible beyond the args of p.div	blob \| commitdiff \| raw \| diff to current
2018-06-10	acondolu	Improved backtracking in Simple	blob \| commitdiff \| raw \| diff to current
2018-06-10	acondolu	Implemented garbage in Num	blob \| commitdiff \| raw \| diff to current
2018-06-10	acondolu	Fix: bug in printing garbage, did not consider the...	blob \| commitdiff \| raw \| diff to current
2018-06-09	acondolu	Added garbage to L	blob \| commitdiff \| raw \| diff to current
2018-06-09	acondolu	Removed eat, p.stepped, p.phase and t.B	blob \| commitdiff \| raw \| diff to current
2018-06-07	acondolu	Using andrea's finish instead of eat. All tests succeed.	blob \| commitdiff \| raw \| diff to current
2018-06-07	acondolu	Trailing constant args in p.div are removed by sanity	blob \| commitdiff \| raw \| diff to current
2018-06-06	Claudio Sacerdoti...	Fix: eating a lambda^n.C args is bad	blob \| commitdiff \| raw \| diff to current
2018-06-06	Claudio Sacerdoti...	Fix: find_eta_difference now works with inerts of arbit...	blob \| commitdiff \| raw \| diff to current
2018-06-01	acondolu	Experimenting with backtracking and stepping on "all...	blob \| commitdiff \| raw \| diff to current
2018-06-01	acondolu	Implementing constants	blob \| commitdiff \| raw \| diff to current
2018-06-01	acondolu	Removed parameter from C	blob \| commitdiff \| raw \| diff to current
2018-06-01	acondolu	More comments and improved find_eta_difference	blob \| commitdiff \| raw \| diff to current
2018-06-01	acondolu	More comments and better variable names	blob \| commitdiff \| raw \| diff to current
2018-05-31	Claudio Sacerdoti...	Make the code OCaml-4.06.1-friendly	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Updated simple with current parser	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Simpler tests in simple_test.ml + Added diverging tests...	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Eat was erasing terms from C that made it diverge	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Bug in mk_app with C	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Fix no_leading_lambdas to account for a step on x on...	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Clean up, improve comments, move functions	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Added check for eta_subterm in `solve'	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Added simple_test.ml	blob \| commitdiff \| raw \| diff to current
2018-05-31	acondolu	Moved andrea.ml to simple.ml	blob \| commitdiff \| raw \| diff to current

Unnamed repository; edit this file 'description' to name the repository.

RSS Atom