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_classes.ml | 4 ++--
 plugins/subtac/subtac_command.ml | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins')

diff --git a/plugins/subtac/subtac_classes.ml b/plugins/subtac/subtac_classes.ml
index 640d3e60d6..38f13a76e6 100644
--- a/plugins/subtac/subtac_classes.ml
+++ b/plugins/subtac/subtac_classes.ml
@@ -34,9 +34,9 @@ let interp_casted_constr_evars evdref env ?(impls=Constrintern.empty_internaliza
   interp_constr_evars_gen evdref env ~impls (OfType (Some typ)) c
 
 let interp_context_evars evdref env params =
-  Constrintern.interp_context_gen
+  let impls_env, bl = Constrintern.interp_context_gen
     (fun env t -> SPretyping.understand_tcc_evars evdref env IsType t)
-    (SPretyping.understand_judgment_tcc evdref) !evdref env params
+    (SPretyping.understand_judgment_tcc evdref) !evdref env params in bl
 
 let type_ctx_instance evars env ctx inst subst =
   let rec aux (subst, instctx) l = function
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