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.

3 files changed, 5 insertions, 5 deletions

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d335836dfc..5056d605dc 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 3f83f104e9..db47a9857d 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 allow_patvar isarity {ltacvars=lfun; genv=env} c =
+let intern_constr_gen pattern_mode 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 allow_patvar isarity {ltacvars=lfun; genv=env} c =
     ltac_bound = Id.Set.empty;
   } 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 50f43931e9..2d5dc58211 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 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;
@@ -624,7 +624,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