From d3a8a8870050810a7bc3fb5e004059197ec364f8 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 8 Apr 2020 13:06:00 +0200 Subject: print hashes --- extraction/extraction.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'extraction') diff --git a/extraction/extraction.v b/extraction/extraction.v index c2b5d83e..72c19385 100644 --- a/extraction/extraction.v +++ b/extraction/extraction.v @@ -152,6 +152,8 @@ Extract Constant Compopts.time => "Timing.time_coq". (*Extraction Inline Compiler.apply_total Compiler.apply_partial.*) (* Profiling *) +Extract Constant AST.profiling_id => "Digest.t". +Extract Constant AST.profiling_id_eq => "Digest.equal". Extract Constant Profiling.function_id => "Profilingaux.function_id". Extract Constant Profiling.branch_id => "Profilingaux.branch_id". -- cgit