GitLab

Use Open/Close Scope without Local (i.e., export the scope opening)
only when the scope corresponds to the main purpose of the module.

Otherwise type class search ocasionally unfolds them and finds
wrong instances. Based on an issue reported by @jihgfee.

This changes the encoding used for finite lists of values of countable
types to be linear instead of exponential. The encoding works by
duplicating bits of each element so that 0 -> 00 and 1 -> 11, and then
separating each element with 10. The top 1-bits are not kept since we
know a 10 is starting a new element which ends with a 1.

Fix #28

Adding a hint without a database now triggers a deprecation warning in
Coq master (https://github.com/coq/coq/pull/8987).

Terminology taken from "A Fresh Look at Separation Algebras and Share"
by Dockins et al.

This gets rid of the old hack to have specific notations for pairs
up to a fixed arity, and moreover allows to do fancy things like:

```
Record test := Test { t1 : nat; t2 : nat }.

Definition foo (x : option test) : option nat :=
  ''(Test a1 a2) ← x;
  Some a1.
```

This allows for more control over `Hint Mode`.

See also Coq bug #5712.

This patch was created using

  find -name *.v | xargs -L 1 awk -i inplace '{from = 0} /^From/{ from = 1; ever_from = 1} { if (from == 0 && seen == 0 && ever_from == 1) { print "Set Default Proof Using \"Type*\"."; seen = 1 } }1 '

and some minor manual editing