From f99150300603ce0d87db716efc52fa88967d4460 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 1 Dec 1999 23:13:01 +0000
Subject: Intégration du Termast et du Retyping de HH, et modifications
 connexes

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@185 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 library/impargs.ml  | 13 +++++++------
 library/impargs.mli | 11 +++++++----
 2 files changed, 14 insertions(+), 10 deletions(-)

(limited to 'library')

diff --git a/library/impargs.ml b/library/impargs.ml
index cd9a5ef4e1..baa9933121 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -82,13 +82,14 @@ let constructor_implicits ((sp,i),j) =
   let imps = Spmap.find sp !inductives_table in
   (snd imps.(i)).(pred j)
 
-let mconstr_implicits mc = 
-  let (sp, i, j, _) = destMutConstruct mc in
-  list_of_implicits (constructor_implicits ((sp,i),j))
+let constructor_implicits_list constr_sp = 
+  list_of_implicits (constructor_implicits constr_sp)
 
-let mind_implicits m =
-  let (sp,i,_) = destMutInd m in
-  list_of_implicits (inductive_implicits (sp,i))
+let inductive_implicits_list ind_sp =
+  list_of_implicits (inductive_implicits ind_sp)
+
+let constant_implicits_list sp =
+  list_of_implicits (constant_implicits sp)
 
 let implicits_of_var kind id =
   failwith "TODO: implicits of vars"
diff --git a/library/impargs.mli b/library/impargs.mli
index 8a598ef7e8..8659b4b408 100644
--- a/library/impargs.mli
+++ b/library/impargs.mli
@@ -4,6 +4,7 @@
 (*i*)
 open Names
 open Term
+open Inductive
 (*i*)
 
 (* Implicit arguments. Here we store the implicit arguments. Notice that we 
@@ -25,10 +26,12 @@ val declare_constant_manual_implicits : section_path -> int list -> unit
 val constant_implicits : section_path -> implicits
 
 val declare_inductive_implicits : section_path -> unit
-val inductive_implicits : section_path * int -> implicits
-val constructor_implicits : (section_path * int) * int -> implicits
+val inductive_implicits : inductive_path -> implicits
+val constructor_implicits : constructor_path -> implicits
+
+val constructor_implicits_list : constructor_path -> int list
+val inductive_implicits_list : inductive_path -> int list
+val constant_implicits_list : section_path -> int list
 
-val mconstr_implicits : constr -> int list
-val mind_implicits : constr -> int list
 val implicits_of_var : Names.path_kind -> identifier -> int list
 
-- 
cgit v1.2.3