From 9c6697d52b62221255830c22d62f16ce08797ddf Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 20 Apr 2000 16:01:22 +0000
Subject: Abstraction du type typed_type (un pas vers les jugements 2 niveaux)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@363 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index 1a9b741c42..d53d576fbe 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -45,7 +45,7 @@ let constants_table = ref Spmap.empty
 
 let declare_constant_implicits sp =
   let cb = Global.lookup_constant sp in
-  let imps = auto_implicits cb.const_type.body in
+  let imps = auto_implicits (body_of_type cb.const_type) in
   constants_table := Spmap.add sp imps !constants_table
 
 let declare_constant_manual_implicits sp imps =
@@ -67,7 +67,7 @@ let inductives_table = ref Spmap.empty
 let declare_inductive_implicits sp =
   let mib = Global.lookup_mind sp in
   let imps_one_inductive mip =
-    (auto_implicits mip.mind_arity.body,
+    (auto_implicits (body_of_type mip.mind_arity),
      let (_,lc) = decomp_all_DLAMV_name mip.mind_lc in
      Array.map auto_implicits lc)
   in
@@ -98,7 +98,7 @@ let var_table = ref Idmap.empty
 
 let declare_var_implicits id = 
   let (_,ty) = Global.lookup_var id in
-  let imps = auto_implicits ty.body in
+  let imps = auto_implicits (body_of_type ty) in
   var_table := Idmap.add id imps !var_table
 
 let implicits_of_var _ id =
-- 
cgit v1.2.3