From e7d592ada2d681876d2bcf0a45d4267b3746064f Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 14 Feb 2001 15:41:55 +0000
Subject: Mise en place d'un système optionnel de discharge immédiat; prise en
 compte des défs locales dans les arguments des inductifs; nettoyage divers

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/cooking.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'kernel/cooking.ml')

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cfbd760d83..f0be35882b 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -145,5 +145,6 @@ let cook_constant env r =
   let cb = lookup_constant r.d_from env in
   let typ = expmod_type env r.d_modlist cb.const_type in
   let body = option_app (expmod_constr env r.d_modlist) cb.const_body in
-  let hyps = map_named_context (expmod_constr env r.d_modlist) cb.const_hyps in
+  let hyps = List.map (fun (sp,c,t) -> (basename sp,c,t)) cb.const_hyps in
+  let hyps = map_named_context (expmod_constr env r.d_modlist) hyps in
   abstract_constant r.d_abstract hyps (body,typ)
-- 
cgit v1.2.3