diff options
| author | Hugo Herbelin | 2017-04-26 12:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-04-28 16:39:54 +0200 |
| commit | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /plugins/ltac/tacintern.ml | |
| parent | 66a68a4329ce199f25184ba8b2d98b4679e7ddae (diff) | |
Renaming allow_patvar flag of intern_gen into pattern_mode.
This highlights that this is a binary mode changing the interpretation
of "?x" rather than additionally allowing patvar.
Diffstat (limited to 'plugins/ltac/tacintern.ml')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3f83f104e9..db47a9857d 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -198,7 +198,7 @@ let intern_binding_name ist x = and if a term w/o ltac vars, check the name is indeed quantified *) x -let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env} c = let warn = if !strict_check then fun x -> x else Constrintern.for_grammar in let scope = if isarity then Pretyping.IsType else Pretyping.WithoutTypeConstraint in let ltacvars = { @@ -206,7 +206,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} c = ltac_bound = Id.Set.empty; } in let c' = - warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c + warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c in (c',if !strict_check then None else Some c) |