diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 13:06:00 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-04-08 13:06:00 +0200 |
| commit | d3a8a8870050810a7bc3fb5e004059197ec364f8 (patch) | |
| tree | 8368172ddd21e31aea993c80a9740e8b1a2d9706 /common/AST.v | |
| parent | cce39d8408cfa33ae4cc7c586e35546a5b731dbf (diff) | |
| download | compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.tar.gz compcert-kvx-d3a8a8870050810a7bc3fb5e004059197ec364f8.zip | |
print hashes
Diffstat (limited to 'common/AST.v')
| -rw-r--r-- | common/AST.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/common/AST.v b/common/AST.v index 846678c2..268e13d5 100644 --- a/common/AST.v +++ b/common/AST.v @@ -465,7 +465,8 @@ Qed. (** * External functions *) (* Identifiers for profiling information *) -Definition profiling_id := Z.t. +Parameter profiling_id : Type. +Axiom profiling_id_eq : forall (x y : profiling_id), {x=y} + {x<>y}. Definition profiling_kind := Z.t. (** For most languages, the functions composing the program are either @@ -577,7 +578,7 @@ Definition ef_reloads (ef: external_function) : bool := Definition external_function_eq: forall (ef1 ef2: external_function), {ef1=ef2} + {ef1<>ef2}. Proof. - generalize ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. + generalize profiling_id_eq ident_eq string_dec signature_eq chunk_eq typ_eq list_eq_dec zeq Int.eq_dec; intros. decide equality. Defined. Global Opaque external_function_eq. |