From f1778f0e830c50aaec250916f14e202d95960414 Mon Sep 17 00:00:00 2001 From: barras Date: Tue, 9 Oct 2001 16:40:03 +0000 Subject: 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 --- library/declare.mli | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) (limited to 'library/declare.mli') diff --git a/library/declare.mli b/library/declare.mli index 5563ebe9e..6918c99db 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -35,7 +35,7 @@ type section_variable_entry = type variable_declaration = section_variable_entry * strength -val declare_variable : identifier -> variable_declaration -> variable_path +val declare_variable : identifier -> variable_declaration -> variable type constant_declaration_type = | ConstantEntry of constant_entry @@ -46,20 +46,20 @@ type constant_declaration = constant_declaration_type * strength (* [declare_constant id cd] declares a global declaration (constant/parameter) with name [id] in the current section; it returns the full path of the declaration *) -val declare_constant : identifier -> constant_declaration -> constant_path +val declare_constant : identifier -> constant_declaration -> constant -val redeclare_constant : constant_path -> constant_declaration -> unit +val redeclare_constant : constant -> constant_declaration -> unit -val declare_parameter : identifier -> constr -> constant_path +val declare_parameter : identifier -> constr -> constant (* [declare_mind me] declares a block of inductive types with their constructors in the current section; it returns the path of the whole block *) -val declare_mind : mutual_inductive_entry -> mutual_inductive_path +val declare_mind : mutual_inductive_entry -> mutual_inductive (* [declare_eliminations sp] declares elimination schemes associated to the mutual inductive block refered by [sp] *) -val declare_eliminations : mutual_inductive_path -> unit +val declare_eliminations : mutual_inductive -> unit val out_inductive : Libobject.obj -> mutual_inductive_entry @@ -70,15 +70,15 @@ val make_strength_2 : unit -> strength (*s Corresponding test and access functions. *) val is_constant : section_path -> bool -val constant_strength : constant_path -> strength -val constant_or_parameter_strength : constant_path -> strength +val constant_strength : constant -> strength +val constant_or_parameter_strength : constant -> strength val out_variable : Libobject.obj -> identifier * variable_declaration -val get_variable : variable_path -> named_declaration * strength +val get_variable : variable -> named_declaration * strength val get_variable_with_constraints : - variable_path -> named_declaration * Univ.constraints * strength -val variable_strength : variable_path -> strength -val find_section_variable : identifier -> variable_path + variable -> named_declaration * Univ.constraints * strength +val variable_strength : variable -> strength +val find_section_variable : identifier -> variable val last_section_hyps : dir_path -> identifier list (*s [global_reference k id] returns the object corresponding to @@ -90,7 +90,7 @@ val last_section_hyps : dir_path -> identifier list given environment instead of looking in the current global environment. *) val context_of_global_reference : global_reference -> section_context -val instantiate_inductive_section_params : constr -> inductive_path -> constr +val instantiate_inductive_section_params : constr -> inductive -> constr val implicit_section_args : global_reference -> section_path list val extract_instance : global_reference -> constr array -> constr array @@ -110,8 +110,8 @@ val construct_reference : Environ.env -> path_kind -> identifier -> constr val is_global : identifier -> bool -val path_of_inductive_path : inductive_path -> mutual_inductive_path -val path_of_constructor_path : constructor_path -> mutual_inductive_path +val path_of_inductive_path : inductive -> mutual_inductive +val path_of_constructor_path : constructor -> mutual_inductive (* Look up function for the default elimination constant *) val elimination_suffix : sorts_family -> string -- cgit v1.2.3