aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp
diff options
context:
space:
mode:
authorGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-26 12:15:26 +0200
committerGravatar Hugo Herbelin <Hugo.Herbelin@inria.fr>2017-04-28 16:39:54 +0200
commit7bdfa1a4e46acf11d199a07bfca0bc59381874c3 (patch)
treef28b3e927cf7715f97f3f31285e4903e426ec362 /interp
parent66a68a4329ce199f25184ba8b2d98b4679e7ddae (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.ml12
-rw-r--r--interp/constrintern.mli2
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 ->