From b6264bb2df9b73b905af126ede49cd31abf0e7da Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 7 Feb 2020 18:13:25 +0100
Subject: Remove the Template Check option.

---
 kernel/declareops.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'kernel/declareops.ml')

diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 047027984d..a3adac7a11 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -26,7 +26,6 @@ let safe_flags oracle = {
   enable_VM = true;
   enable_native_compiler = true;
   indices_matter = true;
-  check_template = true;
 }
 
 (** {6 Arities } *)
-- 
cgit v1.2.3