From 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin <Hugo.Herbelin@inria.fr>
Date: Wed, 26 Apr 2017 12:15:26 +0200
Subject: 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.
---
 interp/constrintern.ml  | 12 ++++++------
 interp/constrintern.mli |  2 +-
 2 files changed, 7 insertions(+), 7 deletions(-)

(limited to 'interp')

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 ->
-- 
cgit v1.2.3