diff options
| author | Hugo Herbelin | 2017-04-26 12:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2017-05-31 02:04:09 +0200 |
| commit | 5dd98189c6554733fe4e22401e1637330cc8a30a (patch) | |
| tree | bc580d37a6d3d20b99c36af84913b7f895f79502 /plugins/ltac/tacintern.ml | |
| parent | bcc9165aec1a80d563d7060ef127ad022e9ed008 (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 e431a13bc2..5cac34e5a2 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -189,7 +189,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; extra} c = +let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} 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 = { @@ -198,7 +198,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c = ltac_extra = extra; } 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) |