From 7bdfa1a4e46acf11d199a07bfca0bc59381874c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
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.
---
 plugins/ltac/tacintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/ltac/tacintern.ml')

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