Fix #1: Port Needle.v to Coq 8.6-8.8

[Blaisorblade]

Problem: Coq >= 8.6 does not recognize the intro pattern (), which also does not
appear documented in Coq 8.5.3 reference
manual. So I guessed what to use instead.

Testing on the examples confirms that they all compile when replacing ()
with [] (which causes a pattern match on the variable namespace). I also tried
? to replace (), but some lemmas failed.

Logistically, this PR only updates the master copy of Needle.v, not the dup in examples/ — PR #4 removes the extra copy anyway.

This fixes #1 enough to allow the generated code to compile (tho with warnings). But the rest of the needle proofs from the ESOP'17 submission fail, and I can't exclude that fixing them require changes to Needle.

Here's one example, with Coq 8.6.0 (tho results seem the same on all proofs across 8.6.0-8.8.2):

/Library/Developer/CommandLineTools/usr/bin/make -j -f Makefile.coq
COQC LambdaOmega.v
File "./LambdaOmega.v", line 2043, characters 0-2410:
Warning: Not a fully mutually defined fixpoint
(e.g., TRed_wf_1 and TRed_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2070, characters 0-1157:
Warning: Not a fully mutually defined fixpoint
(Kinding_wf_1 and Kinding_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2086, characters 0-1056:
Warning: Not a fully mutually defined fixpoint
(e.g., TRedStar_wf_1 and TRedStar_wf_0 are not mutually
dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2104, characters 0-2740:
Warning: Not a fully mutually defined fixpoint
(TyEq_wf_2 and TyEq_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2137, characters 0-1148:
Warning: Not a fully mutually defined fixpoint
(Typing_wf_1 and Typing_wf_0 are not mutually dependent).
Well-foundedness check may fail unexpectedly.
 [non-full-mutual,fixpoints]
File "./LambdaOmega.v", line 2181, characters 0-61:
Warning: obligation_Env_reg_TRed is declared as a local axiom
[local-declaration,scope]
COQC DeclarationEvaluation.v
COQC MetaTheory.v
File "./MetaTheory.v", line 278, characters 4-56:
Error: Unable to find an instance for the variables S1, S2.
make[2]: *** [MetaTheory.vo] Error 1
make[2]: Target `all' not remade because of errors.
make[1]: *** [coq] Error 2
make: *** [lomega] Error 2

I took the liberty of uploading to https://github.com/Blaisorblade/knot-esop-2017-case-study/ for convenience, tho strictly speaking nobody can use those files as they have no license.

[Blaisorblade]

Here's a log of the results of the evaluation with this fix: https://gist.github.com/Blaisorblade/60bf54e17c08ce82e53427e7fa3858f0/696b6665c9f83ff516d8160a4c394c9ba5c02c66