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.

5 files changed, 12 insertions, 12 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 4dcf287efc..d4d8299701 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1506,7 +1506,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 = CAst.with_loc_val (fun ?loc -> function
     | CRef (ref,us) ->
 	let (c,imp,subscopes,l),_ =
@@ -1749,10 +1749,10 @@ let internalize globalenv env allow_patvar (_, ntnvars as lvar) c =
 	CAst.make ?loc @@
 	GHole (k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar n when allow_patvar ->
+    | CPatVar n when pattern_mode ->
 	CAst.make ?loc @@
 	GPatVar (true,n)
-    | CEvar (n, []) when allow_patvar ->
+    | CEvar (n, []) when pattern_mode ->
 	CAst.make ?loc @@
 	GPatVar (false,n)
     (* end *)
@@ -1944,13 +1944,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
 
@@ -2023,7 +2023,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 644cafe575..723bb68b6a 100644
--- a/interp/constrintern.mli
+++ b/interp/constrintern.mli
@@ -83,7 +83,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 ->
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 74c0eb4cc7..72d29f5e07 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -142,7 +142,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits env sigma impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    ~allow_patvar:false c
+    c
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index e431a13bc2..5cac34e5a2 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -189,7 +189,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 allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
+let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env; extra} 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 = {
@@ -198,7 +198,7 @@ let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env; extra} c =
     ltac_extra = extra;
   } in
   let c' =
-    warn (Constrintern.intern_gen scope ~allow_patvar ~ltacvars env) c
+    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c
   in
   (c',if !strict_check then None else Some c)
 
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index a9ec779d11..627f495d65 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -589,7 +589,7 @@ let interp_uconstr ist env sigma = function
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
-let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
+let interp_gen kind ist pattern_mode flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_context ist env sigma in
   let vars = {
     Pretyping.ltac_constrs = constrvars.typed;
@@ -617,7 +617,7 @@ let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
-      intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
+      intern_gen kind_for_intern ~pattern_mode ~ltacvars env c
   in
   (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
       suggested by Arnaud Spiwack, we run push_trace immediately.  We do