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

1 files changed, 15 insertions, 15 deletions

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