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.

---
 checker/checkInductive.ml | 1 -
 1 file changed, 1 deletion(-)

(limited to 'checker/checkInductive.ml')

diff --git a/checker/checkInductive.ml b/checker/checkInductive.ml
index 051f51bbb3..62e732ce69 100644
--- a/checker/checkInductive.ml
+++ b/checker/checkInductive.ml
@@ -170,7 +170,6 @@ let check_inductive env mind mb =
          check_guarded = mb_flags.check_guarded;
          check_positive = mb_flags.check_positive;
          check_universes = mb_flags.check_universes;
-         check_template = mb_flags.check_template;
          conv_oracle = mb_flags.conv_oracle;
         }
         env
-- 
cgit v1.2.3