From d3a8a8870050810a7bc3fb5e004059197ec364f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 13:06:00 +0200 Subject: print hashes --- common/AST.v | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) (limited to 'common/AST.v') 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. -- cgit