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

6 files changed, 43 insertions, 48 deletions

diff --git a/library/declare.ml b/library/declare.ml
index b10658466e..19c7323c9f 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -459,18 +459,17 @@ let constr_of_reference _ _ ref =
 if Options.immediate_discharge then
   match ref with
     | VarRef sp -> mkVar (basename sp)
-    | ConstRef sp -> mkConst (sp,[||])
-    | ConstructRef sp -> mkMutConstruct (sp,[||])
-    | IndRef sp -> mkMutInd (sp,[||])
+    | ConstRef sp -> mkConst sp
+    | ConstructRef sp -> mkMutConstruct sp
+    | IndRef sp -> mkMutInd sp
 else
   let hyps = context_of_global_reference ref in
   let hyps0 = current_section_context () in
-  let args = instance_from_section_context hyps in
   let body = match ref with
     | VarRef sp -> mkVar (basename sp)
-    | ConstRef sp -> mkConst (sp,Array.of_list args)
-    | ConstructRef sp -> mkMutConstruct (sp,Array.of_list args)
-    | IndRef sp -> mkMutInd (sp,Array.of_list args)
+    | ConstRef sp -> mkConst sp
+    | ConstructRef sp -> mkMutConstruct sp
+    | IndRef sp -> mkMutInd sp
   in
   find_common_hyps_then_abstract body hyps0 hyps
 
@@ -565,7 +564,7 @@ let declare_one_elimination mispec =
   let mindstr = string_of_id (mis_typename mispec) in
   let declare na c =
     (* Hack to get const_hyps right in the declaration *)
-    let c = instantiate_inductive_section_params c (fst (mis_inductive mispec))
+    let c = instantiate_inductive_section_params c (mis_inductive mispec)
     in
     let _ = declare_constant (id_of_string na)
       (ConstantEntry
@@ -594,16 +593,15 @@ let declare_eliminations sp =
   if not (list_subset ids (ids_of_named_context (Global.named_context ()))) then    error ("Declarations of elimination scheme outside the section "^
     "of the inductive definition is not implemented");
 *)
-  let ctxt = instance_from_section_context mib.mind_hyps in
   for i = 0 to Array.length mib.mind_packets - 1 do
     if mind_type_finite mib i then
-      let mispec = Global.lookup_mind_specif ((sp,i), Array.of_list ctxt) in 
+      let mispec = Global.lookup_mind_specif (sp,i) in 
       declare_one_elimination mispec
   done
 
 (* Look up function for the default elimination constant *)
 
-let lookup_eliminator env (ind_sp,_) s =
+let lookup_eliminator env ind_sp s =
   let path = path_of_inductive_path ind_sp in
   let dir, base,k = repr_path path in
   let id = add_suffix base (elimination_suffix s) in
diff --git a/library/declare.mli b/library/declare.mli
index 5563ebe9e9..6918c99db3 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
diff --git a/library/impargs.ml b/library/impargs.ml
index d71acd70fc..63351392ee 100644
--- a/library/impargs.ml
+++ b/library/impargs.ml
@@ -126,7 +126,7 @@ let constant_implicits_list sp =
    implicit arguments of the constructors. *)
 
 module Inductive_path = struct
-  type t = inductive_path
+  type t = inductive
   let compare (spx,ix) (spy,iy) = 
     let c = ix - iy in if c = 0 then sp_ord spx spy else c
 end
@@ -136,7 +136,7 @@ module Indmap = Map.Make(Inductive_path)
 let inductives_table = ref Indmap.empty
 
 module Construtor_path = struct
-  type t = constructor_path
+  type t = constructor
   let compare (indx,ix) (indy,iy) = 
     let c = ix - iy in if c = 0 then Inductive_path.compare indx indy else c
 end
@@ -269,18 +269,15 @@ let context_of_global_reference = function
   | ConstructRef ((sp,_),_) -> (Global.lookup_mind sp).mind_hyps
 
 let type_of_global r =
-  let args = 
-    Array.of_list
-      (Sign.instance_from_section_context (context_of_global_reference r)) in
   match r with
   | VarRef sp ->
       lookup_named_type (basename sp) (Global.env ())
   | ConstRef sp ->
-      Typeops.type_of_constant (Global.env ()) Evd.empty (sp,args)
+      Typeops.type_of_constant (Global.env ()) Evd.empty sp
   | IndRef sp -> 
-      Typeops.type_of_inductive (Global.env ()) Evd.empty (sp,args)
+      Typeops.type_of_inductive (Global.env ()) Evd.empty sp
   | ConstructRef sp ->
-      Typeops.type_of_constructor (Global.env ()) Evd.empty (sp,args)
+      Typeops.type_of_constructor (Global.env ()) Evd.empty sp
 
 let check_range n i =
   if i<1 or i>n then error ("Bad argument number: "^(string_of_int i))
diff --git a/library/impargs.mli b/library/impargs.mli
index 9b8d0616d9..ceaa30cdff 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
 
diff --git a/library/indrec.ml b/library/indrec.ml
index 96a188da79..36ce4f783c 100644
--- a/library/indrec.ml
+++ b/library/indrec.ml
@@ -319,7 +319,7 @@ let mis_make_indrec env sigma listdepkind mispec =
 	      it_mkLambda_or_LetIn_name env
 		(lambda_create env
 		   (build_dependent_inductive
-		      (lift_inductive_family nrec indf),
+                     (lift_inductive_family nrec indf),
 		    mkMutCase (make_default_case_info mispeci,
 			       mkRel (dect+j+1), mkRel 1, branches)))
 		(Sign.lift_rel_context nrec lnames)
@@ -443,13 +443,13 @@ let check_arities listdepkind =
 
 let build_mutual_indrec env sigma = function 
   | (mind,dep,s)::lrecspec ->
-      let ((sp,tyi),_) = mind in
+      let (sp,tyi) = mind in
       let mispec = lookup_mind_specif mind env in
       let listdepkind = 
     	(mispec, dep,s)::
     	(List.map
 	   (function (mind',dep',s') ->
-	      let ((sp',_),_) = mind' in
+	      let (sp',_) = mind' in
 	      if sp=sp' then 
 		(lookup_mind_specif mind' env,dep',s') 
 	      else 
diff --git a/library/nametab.mli b/library/nametab.mli
index 7d0f164f97..f34895befe 100755
--- a/library/nametab.mli
+++ b/library/nametab.mli
@@ -70,7 +70,7 @@ val extended_locate : qualid -> extended_global_reference
 
 val locate_obj : qualid -> section_path
 
-val locate_constant : qualid -> constant_path
+val locate_constant : qualid -> constant
 val locate_section : qualid -> dir_path
 
 (* [exists sp] tells if [sp] is already bound to a cci term *)