Removing explicit substitutions
Problems of sort
Dealing with universes inconsistencies
Not working
A git ignore
Merge of various commits by Pierre:

- Training whitespace + cma construction + env update + mkApp fix

- diag calls diag in return clause without apparent deBruijn
  mess. Next step is to erase impossible branch at toplevel like we do
  in recursive calls Then we'll have to generalize automaticaly stuff
  in the context we share dependences

- Commentary update

- the lifts to get a as correct as possible test6.vo are back

- Clean example and add one to show that stt is not the correct datastructure

- diag now works on a return type instead of a telescope
Makefile cleanup + invert_tactic2 erasure (Wasting 1 hour because doing our own makefile is faster)

mk_casei + drop useless stuff + elementary bricks reorganisation
A new version of the internal representation: we merge the former list
of variables and the split trees.

In the end, the split tree list can be seen as a term with holes: we
could go one step forward and drop this notion altogether, and
represent the split trees as regular coq terms.
Final commit on this branch (cleaning)