From 33d7e374b449c754fcdf623e98cb717faaf241a5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 4 Dec 2017 17:45:50 +0100
Subject: Fixup strict mode for patterns

---
 src/tac2core.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/tac2core.ml b/src/tac2core.ml
index fe4912a6c5..32c873088c 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -895,7 +895,8 @@ let () =
   let intern self ist c =
     let env = ist.Genintern.genv in
     let sigma = Evd.from_env env in
-    let _, pat = Constrintern.intern_constr_pattern env sigma ~as_type:false c in
+    let warn = if !Ltac_plugin.Tacintern.strict_check then fun x -> x else Constrintern.for_grammar in
+    let _, pat = warn (fun () ->Constrintern.intern_constr_pattern env sigma ~as_type:false c) () in
     GlbVal pat, gtypref t_pattern
   in
   let print env pat = str "pattern:(" ++ Printer.pr_lconstr_pattern_env env Evd.empty pat ++ str ")" in
-- 
cgit v1.2.3