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.
---
 interp/constrintern.mli | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'interp/constrintern.mli')

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