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/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/funind')

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