In the construction of diag, we test whether a branch is eliminated by
the return clause of the match, and in that case, we instantiate it
with False_rect.
In fact the concl argument must be local to each call of build. (This
commit is done to prepare for the next one.)
At the toplevel, we must transform var into rels (the subtitution),
but deeper in the diag, we must transform rels into rels.

Therefore, we backtrack on the previous commit, to forget about
substitutions and shifts, and solely use the conclusion term.
A good moment to take a break
Universe inconsistency
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)
Integrating the new internal representation for split trees: this
makes it possible to make test6 go through (re generalizing the
dependencies).