The first one is the main file, the rest only supply
rules for individual theories and modules.

in anticipation of future module refinement

features polymorphic recursion, both in the logic and in programs

Expr: separate first-order "expr" and higher-order "cexp"
Dexpr: add an "absurd" branch for non-exhaustive matches in programs

        introduced in cc774eb2

When coqtop -config return something like

```
CAMLP4OPTIONS=-loc loc
```

(cf https://coq.inria.fr/bugs/show_bug.cgi?id=4163)