diff options
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 |