Optimization: in case of empty substitution, merging is trivial.
Adding Acc_intro_generator in order to help computations of Function in particular
Add Acc_intro_generator on top of all wf function proof (much much faster execution)
updated .mailmap
Field_theory: nicer notations for constants 0 1 ...
Fix various \r issues with windows

Also add a 2 in an error message (it's gSourceView2, not gSourceView).

This closes bugs 3150, 3151, 3152, and 3153.
configure: fix some issues with last commit

 - after piping with | tr -d, an exit code was lost
 - suspicious use of " " inside a larger " ", we use ' ' now instead
configure: CAML_LD_LIBRARY_PATH is enriched, not overwritten

 Keeping the earlier content of this variable is crucial for opam
 (at least).

 Thanks to François Bobot and Thomas Refis for this one...
Using hashes instead of strings in dynamic tags. In case of collision, an
anomaly is raised. As there are very few tags defined in Coq code, this is
very unlikely to appear, and can be fixed by tweaking the name of the
dynamic argument.

This should be more efficient, as we did compare equal strings each time.
Using hashes in Summary, like the previous commit did with Dyn.
configure: improve last fix

 Let's avoid the "if a=$(cmd ...)" since:
 - unless being a shell expert, it's not obvious it's testing the exit code
   of cmd.
 - it's quite fragile, if you pipe cmd into a cmd2 you'll lose the
   exit code of cmd.

 Instead, we test the emptiness of the variable content afterwards
Adding generic solvers to term holes. For now, no resolution mechanism nor
parsing is plugged.
Adding the necessary hooks to handle tactics in terms.
Actually adding the grammar entry to handle tactics in terms.