Fixed costly general recursive rhs modality instance, partially fixed running TC search too often for recursive hint search.

Fixed actris nasty unification trouble, made solveone responsible for close_token, added sketch of mergablepersenv in introducehyp.

Separated int_as_nat_diff library, extra pure hints no longer need ugly ltac overriding, improved spin and ticket lock allocation specs.

Removed normalization in definitions, hyp_first instance on disjunctions is working. Need to fix inc_dec, fork_join, benchmark.