Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."

This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.

5 files changed, 12 insertions, 12 deletions

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 94924374a8..d75487ecf3 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 pattern_mode (_, ntnvars as lvar) c =
+let internalize globalenv env allow_patvar (_, 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 pattern_mode (_, ntnvars as lvar) c =
         in
 	GHole (loc, k, naming, solve)
     (* Parsing pattern variables *)
-    | CPatVar (loc, n) when pattern_mode ->
+    | CPatVar (loc, n) when allow_patvar ->
 	GPatVar (loc, (true,n))
-    | CEvar (loc, n, []) when pattern_mode ->
+    | CEvar (loc, n, []) when allow_patvar ->
 	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) ?(pattern_mode=false) ?(ltacvars=empty_ltac_sign)
+               ?(impls=empty_internalization_env) ?(allow_patvar=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}
-    pattern_mode (ltacvars, Id.Map.empty) c
+    allow_patvar (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)
-            ~pattern_mode:true ~ltacvars env c in
+            ~allow_patvar: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 2142d42bce..758d4e650b 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 -> ?pattern_mode:bool -> ?ltacvars:ltac_sign ->
+  ?impls:internalization_env -> ?allow_patvar: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 5056d605dc..d335836dfc 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
-    c
+    ~allow_patvar:false c
 
 (*
    Construct a fixpoint as a Glob_term
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index db47a9857d..3f83f104e9 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -198,7 +198,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 pattern_mode isarity {ltacvars=lfun; genv=env} c =
+let intern_constr_gen allow_patvar isarity {ltacvars=lfun; genv=env} 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 = {
@@ -206,7 +206,7 @@ let intern_constr_gen pattern_mode isarity {ltacvars=lfun; genv=env} c =
     ltac_bound = Id.Set.empty;
   } in
   let c' =
-    warn (Constrintern.intern_gen scope ~pattern_mode ~ltacvars env) c
+    warn (Constrintern.intern_gen scope ~allow_patvar ~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 2d5dc58211..50f43931e9 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -597,7 +597,7 @@ let interp_uconstr ist env sigma = function
       } in
       { closure ; term =  intern_gen WithoutTypeConstraint ~ltacvars env ce }
 
-let interp_gen kind ist pattern_mode flags env sigma (c,ce) =
+let interp_gen kind ist allow_patvar flags env sigma (c,ce) =
   let constrvars = extract_ltac_constr_context ist env sigma in
   let vars = {
     Pretyping.ltac_constrs = constrvars.typed;
@@ -624,7 +624,7 @@ let interp_gen kind ist pattern_mode flags env sigma (c,ce) =
       } in
       let kind_for_intern =
         match kind with OfType _ -> WithoutTypeConstraint | _ -> kind in
-      intern_gen kind_for_intern ~pattern_mode ~ltacvars env c
+      intern_gen kind_for_intern ~allow_patvar ~ltacvars env c
   in
   (* Jason Gross: To avoid unnecessary modifications to tacinterp, as
       suggested by Arnaud Spiwack, we run push_trace immediately.  We do