diff options
| author | Maxime Dénès | 2017-04-28 22:15:06 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-04-28 22:15:06 +0200 |
| commit | 1c8ed18d5f67d7d5656342584b8dcf8a441cb87f (patch) | |
| tree | ce90c93341c58e82813da8b1a567ce6a3f3ed424 /plugins/ltac/tacintern.ml | |
| parent | 4f742e14441581ece247d33020055f15732f126b (diff) | |
Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."
This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
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 db47a9857d..3f83f104e9 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 pattern_mode isarity {ltacvars=lfun; genv=env} c = +let intern_constr_gen allow_patvar 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 pattern_mode isarity {ltacvars=lfun; genv=env} c = ltac_bound = Id.Set.empty; } in let c' = - warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c + warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c in (c',if !strict_check then None else Some c) |