From 1c8ed18d5f67d7d5656342584b8dcf8a441cb87f Mon Sep 17 00:00:00 2001
From: Maxime Dénès
Date: Fri, 28 Apr 2017 22:15:06 +0200
Subject: Revert "Renaming allow_patvar flag of intern_gen into pattern_mode."

This reverts commit 7bdfa1a4e46acf11d199a07bfca0bc59381874c3.
---
 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 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)
 
-- 
cgit v1.2.3