automatic introduction of hyps

[gares]

The history is a bit messy, but this Fix #5 The split into multiple files is perfectible, there is still some duplicate code. Unfortunately I found a bug in coq-elpi 1.10.0, so this depends on 1.10.1 which is in the making

[gares]

I've reworked the PR, it should have less conflicts.

[gares]

OK, it seems to work. The doc on the Elpi side is still a bit skinny, so I'll sum up it here. Since 1.10 "tactic arguments" are not passed to the tactic, but rather attached to a goal. This solves two problems of the ml API for tactics (the infamous Proofview.tactic monad which type parameter is always set to unit):

• data is where it belongs (a goal is sealed under its bound variables and typing context, a term argument must live in that context, not in the context of the caller)
• a tactic can pass data to the next tactic by putting it in the goal(s) it leaves open

The new code repeat a tactic which does intro and passes to the next tactic the hypothesis just introduced, in this way field finds in his list of arguments all the hyps that were introduced so far.

If this behavior is what we want for the defective field. tactic, then we can merge this.