diff options
| author | herbelin | 1999-12-01 23:13:01 +0000 |
|---|---|---|
| committer | herbelin | 1999-12-01 23:13:01 +0000 |
| commit | f99150300603ce0d87db716efc52fa88967d4460 (patch) | |
| tree | 4a85be13031030ac01659359b032411bfd63a73b /library | |
| parent | 3a49dbf016e1ebf8f8d12ed43fde14c5619ca55e (diff) | |
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
Diffstat (limited to 'library')
| -rw-r--r-- | library/impargs.ml | 13 | ||||
| -rw-r--r-- | library/impargs.mli | 11 |
2 files changed, 14 insertions, 10 deletions
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 |