diff options
| author | Pierre-Marie Pédrot | 2017-12-04 17:45:50 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-03-27 10:32:07 +0200 |
| commit | 33d7e374b449c754fcdf623e98cb717faaf241a5 (patch) | |
| tree | 74e1995c2c97a2add345d26264cc642e916e91a7 | |
| parent | 797cd88b4ea91780fca394a12044f9613ed63fc6 (diff) | |
Fixup strict mode for patterns
| -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 |