diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-26 12:15:26 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-04-28 16:39:54 +0200 |
| commit | 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (patch) | |
| tree | f28b3e927cf7715f97f3f31285e4903e426ec362 /interp | |
| 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')
| -rw-r--r-- | interp/constrintern.ml | 12 | ||||
| -rw-r--r-- | interp/constrintern.mli | 2 |
2 files changed, 7 insertions, 7 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index d75487ecf..94924374a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -1516,7 +1516,7 @@ let extract_explicit_arg imps args = (**********************************************************************) (* Main loop *) -let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = +let internalize globalenv env pattern_mode (_, ntnvars as lvar) c = let rec intern env = function | CRef (ref,us) as x -> let (c,imp,subscopes,l),_ = @@ -1747,9 +1747,9 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c = in GHole (loc, k, naming, solve) (* Parsing pattern variables *) - | CPatVar (loc, n) when allow_patvar -> + | CPatVar (loc, n) when pattern_mode -> GPatVar (loc, (true,n)) - | CEvar (loc, n, []) when allow_patvar -> + | CEvar (loc, n, []) when pattern_mode -> GPatVar (loc, (false,n)) (* end *) (* Parsing existential variables *) @@ -1934,13 +1934,13 @@ let empty_ltac_sign = { } let intern_gen kind env - ?(impls=empty_internalization_env) ?(allow_patvar=false) ?(ltacvars=empty_ltac_sign) + ?(impls=empty_internalization_env) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign) c = let tmp_scope = scope_of_type_kind kind in internalize env {ids = extract_ids env; unb = false; tmp_scope = tmp_scope; scopes = []; impls = impls} - allow_patvar (ltacvars, Id.Map.empty) c + pattern_mode (ltacvars, Id.Map.empty) c let intern_constr env c = intern_gen WithoutTypeConstraint env c @@ -2013,7 +2013,7 @@ let interp_type_evars env evdref ?(impls=empty_internalization_env) c = let intern_constr_pattern env ?(as_type=false) ?(ltacvars=empty_ltac_sign) c = let c = intern_gen (if as_type then IsType else WithoutTypeConstraint) - ~allow_patvar:true ~ltacvars env c in + ~pattern_mode:true ~ltacvars env c in pattern_of_glob_constr c let interp_notation_constr ?(impls=empty_internalization_env) nenv a = diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 758d4e650..2142d42bc 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 -> |