GitLab

Asmgenproof.v: first outline-complete version of the proofs for the new compiler (IntrinSec extended with Reset, using a syntactic notion of straightline code); there are still a few non-trivial admits in the simulation proof (in Mcond_false_case and in step_simulation)

Asm.v: changed def of valid_mask_at_reg, to overcome problem with match_states; Asmgenproof.v: in progress

Asmgenproof1.v: copied from Asmgenproof1SYNT2.v; old version left as Asmgenproof1SEM.v; Asmgenproof.v: in progress

The Commandline module is reusable in other projects, and its license
(GPL) allows such reuse, so its natural place is in lib/ rather
than in driver/

Closes: #351

The corresponding files in all other ports are dual-licensed
(GPL + non-commercial), there is no reason it should be different for
aarch64.

So as not to depend on an implicit import from module Program.
(See PR #352.)

On some versions of Coq, "nil" is of type "Rlist"...

This reverts commit f070949a.

The rest of the code base uses `nil`, so let's be consistent.
Also, this avoids depending on `Import ListNotations`.

import ListNotations wherever it is necessary so that we do not rely on it being exported by Program.  (See #352.)

This is a backport from upstream: https://gitlab.inria.fr/fpottier/menhir/-/commit/53f94fa42c80ab1728383e9d2b19006180b14a78

The file contains various parameters about the target processor and ABI,
useful for VST and possibly other users of CompCert as a Coq library.

It is in "var=val" syntax so that it can be included directly from
a Makefile or a shell script.