diff options
| -rw-r--r-- | src/tac2core.ml | 3 |
1 files changed, 2 insertions, 1 deletions
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 |