From b9f3f8eda83ccfee7f7196f8f4d7584fb1cd9940 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Tue, 2 Apr 2019 14:42:31 +0200
Subject: coqchk: use unsafe marshal for dependencies of -norec libraries

on test-suite/arithmetic/mod: 2.6s to 0.45s
---
 checker/check.ml | 4 ++++
 1 file changed, 4 insertions(+)

(limited to 'checker/check.ml')

diff --git a/checker/check.ml b/checker/check.ml
index 76f85c86c9..a2c8a0f25d 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -328,6 +328,10 @@ let intern_from_file ~intern_mode (dir, f) =
   Flags.if_verbose chk_pp (str"[intern "++str f++str" ...");
   let (sd,md,table,opaque_csts,digest) =
     try
+      let marshal_in_segment f ch = if intern_mode <> Dep
+        then marshal_in_segment f ch
+        else System.marshal_in_segment f ch
+      in
       let ch = System.with_magic_number_check raw_intern_library f in
       let (sd:summary_disk), _, digest = marshal_in_segment f ch in
       let (md:library_disk), _, digest = marshal_in_segment f ch in
-- 
cgit v1.2.3