diff options
| author |  barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
|---|---|---|
| committer | barras <barras@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2001-10-09 16:40:03 +0000 |
| commit | f1778f0e830c50aaec250916f14e202d95960414 (patch) | |
| tree | ae220556180dfa55d6b638467deb7edf58d4c17b /library/impargs.mli | |
| parent | 8dbab7f463cabfc2913ab8615973c96ac98bf371 (diff) | |
Suppression des arguments sur les constantes, inductifs et constructeurs
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library/impargs.mli')
| -rw-r--r-- | library/impargs.mli | 20 |
1 files changed, 10 insertions, 10 deletions
diff --git a/library/impargs.mli b/library/impargs.mli index 9b8d0616d..ceaa30cdf 100644 --- a/library/impargs.mli +++ b/library/impargs.mli @@ -33,9 +33,9 @@ val compute_implicits : env -> 'a Evd.evar_map -> types -> implicits_list (*s Computation of implicits (done using the global environment). *) -val declare_var_implicits : variable_path -> unit -val declare_constant_implicits : constant_path -> unit -val declare_mib_implicits : mutual_inductive_path -> unit +val declare_var_implicits : variable -> unit +val declare_constant_implicits : constant -> unit +val declare_mib_implicits : mutual_inductive -> unit val declare_implicits : global_reference -> unit (* Manual declaration of which arguments are expected implicit *) @@ -43,15 +43,15 @@ val declare_manual_implicits : global_reference -> implicits_list -> unit (*s Access to already computed implicits. *) -val constructor_implicits_list : constructor_path -> implicits_list -val inductive_implicits_list : inductive_path -> implicits_list -val constant_implicits_list : constant_path -> implicits_list +val constructor_implicits_list : constructor -> implicits_list +val inductive_implicits_list : inductive -> implicits_list +val constant_implicits_list : constant -> implicits_list -val implicits_of_var : variable_path -> implicits_list +val implicits_of_var : variable -> implicits_list -val is_implicit_constant : constant_path -> bool -val is_implicit_inductive_definition : inductive_path -> bool -val is_implicit_var : variable_path -> bool +val is_implicit_constant : constant -> bool +val is_implicit_inductive_definition : inductive -> bool +val is_implicit_var : variable -> bool val implicits_of_global : global_reference -> implicits_list |