From 67500967edf584fcddc41c74aea09d48ee80a03c Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 2 Aug 2014 16:34:30 +0200
Subject: Better struture for Ltac internalization environments in
 Constrintern.

---
 plugins/funind/indfun.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins')

diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 2ceda4f48c..808b2604c7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -132,7 +132,7 @@ let rec abstract_glob_constr c = function
 
 let interp_casted_constr_with_implicits sigma env impls c  =
   Constrintern.intern_gen Pretyping.WithoutTypeConstraint env ~impls
-    ~allow_patvar:false  ~ltacvars:(Id.Set.empty, Id.Set.empty,Id.Map.empty) c
+    ~allow_patvar:false c
 
 (*
    Construct a fixpoint as a Glob_term
-- 
cgit v1.2.3