[ porting from CerCo's Matita ]

[ porting from CerCo's Matita ]
1. new implementation of normalize to have a speed up in case of fully applicative terms
2. all reduction tactics used to end with instatiate that re-checked the conversion using
   unification (!!!); added a new flag ?(refine=true) to instantiate to avoid this expensive
   check when we know it is useless