From 35846ec22445e14cb044ef3beb62f5c559d94752 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Nov 2012 03:09:23 +0000
Subject: Taking into account the type of a definition (if it exists), and the
 type in "cast" to activate the temporary interpretation scope.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15978 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 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 48ed144730..6a7a588d48 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -133,7 +133,7 @@ let rec abstract_glob_constr c = function
         (abstract_glob_constr c bl)
 
 let interp_casted_constr_with_implicits sigma env impls c  =
-  Constrintern.intern_gen false sigma env ~impls
+  Constrintern.intern_gen (Pretyping.OfType None) sigma env ~impls
     ~allow_patvar:false  ~ltacvars:([],[]) c
 
 (*
-- 
cgit v1.2.3