From c5fa08bbecbc665e1d82d38d2e41f5256efcd545 Mon Sep 17 00:00:00 2001
From: pboutill
Date: Thu, 10 Feb 2011 14:11:07 +0000
Subject: Interp a definition with the implicit arguments of its local context

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13825 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/subtac/subtac_command.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/subtac/subtac_command.ml')

diff --git a/plugins/subtac/subtac_command.ml b/plugins/subtac/subtac_command.ml
index 6fe31646ba..f02e83ad1a 100644
--- a/plugins/subtac/subtac_command.ml
+++ b/plugins/subtac/subtac_command.ml
@@ -96,7 +96,7 @@ let interp_binder sigma env na t =
     SPretyping.understand_tcc_evars sigma env IsType (locate_if_isevar (loc_of_glob_constr t) na t)
 
 let interp_context_evars evdref env params =
-  let bl = Constrintern.intern_context false !evdref env params in
+  let int_env, bl = Constrintern.intern_context false !evdref env Constrintern.empty_internalization_env params in
   let (env, par, _, impls) =
     List.fold_left
       (fun (env,params,n,impls) (na, k, b, t) ->
-- 
cgit v1.2.3