From 5dd98189c6554733fe4e22401e1637330cc8a30a 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/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 74c0eb4cc7..72d29f5e07 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
-- 
cgit v1.2.3