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 /interp/constrintern.mli | |
| 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 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 758d4e650b..2142d42bce 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -82,7 +82,7 @@ val intern_constr : env -> constr_expr -> glob_constr val intern_type : env -> constr_expr -> glob_constr val intern_gen : typing_constraint -> env -> - ?impls:internalization_env -> ?allow_patvar:bool -> ?ltacvars:ltac_sign -> + ?impls:internalization_env -> ?pattern_mode:bool -> ?ltacvars:ltac_sign -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> |