Introduction constant_path = section_path

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@870 85f007b7-540e-0410-9357-904b9bb8a0f7

5 files changed, 35 insertions, 27 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 8d65e66d27..7aa464db5b 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -34,7 +34,7 @@ let stop() =
 (* [r_const=(false,cl)] means only those in [cl] *)
 type reds = {
   r_beta : bool;
-  r_const : bool * section_path list;
+  r_const : bool * constant_path list;
   r_zeta : bool;
   r_evar : bool;
   r_iota : bool }
@@ -89,7 +89,7 @@ let unfold_red sp = {
 
 type red_kind =
     BETA | DELTA | ZETA | EVAR | IOTA
-  | CONST of section_path list | CONSTBUT of section_path list
+  | CONST of constant_path list | CONSTBUT of constant_path list
 
 let rec red_add red = function
   | BETA -> { red with r_beta = true }
@@ -339,7 +339,7 @@ type cbv_value =
   | LAM of name * constr * constr * cbv_value subs
   | FIXP of fixpoint * cbv_value subs * cbv_value list
   | COFIXP of cofixpoint * cbv_value subs * cbv_value list
-  | CONSTR of int * (section_path * int) * cbv_value array * cbv_value list
+  | CONSTR of int * inductive_path * cbv_value array * cbv_value list
 
 (* les vars pourraient etre des constr,
    cela permet de retarder les lift: utile ?? *) 
diff --git a/kernel/names.ml b/kernel/names.ml
index b5e58c6bfa..8205c564e4 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -192,6 +192,7 @@ module Spmap = Map.Make(SpOrdered)
 
 (* Special references for inductive objects *)
 
+type constant_path = section_path
 type inductive_path = section_path * int
 type constructor_path = inductive_path * int
 
diff --git a/kernel/names.mli b/kernel/names.mli
index 6ae0f515fb..79f5f0e931 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -91,6 +91,7 @@ module Spset : Set.S with type elt = section_path
 module Spmap : Map.S with type key = section_path
 
 (*s Specific paths for declarations *)
+type constant_path = section_path
 type inductive_path = section_path * int
 type constructor_path = inductive_path * int
 
diff --git a/kernel/term.ml b/kernel/term.ml
index d331df98bb..1751c5d82d 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -36,6 +36,15 @@ let print_sort = function
   | Prop Null -> [< 'sTR "Prop" >]
   | Type _ -> [< 'sTR "Type" >]
 
+(********************************************************************)
+(* type of global reference *)
+
+type global_reference =
+  | VarRef of section_path
+  | ConstRef of constant_path
+  | IndRef of inductive_path
+  | ConstructRef of constructor_path
+  | EvarRef of int
 
 (********************************************************************)
 (*       Constructions as implemented                               *)
@@ -114,7 +123,7 @@ struct
 type constr = kind_of_term
 
 and existential = existential_key * constr array
-and constant = section_path * constr array
+and constant = constant_path * constr array
 and constructor = constructor_path * constr array
 and inductive = inductive_path * constr array
 and rec_declaration = constr array * name list * constr array
@@ -314,15 +323,6 @@ type hnftype =
   | HnfAtom   of constr
   | HnfMutInd of inductive * constr array
 
-(***********************************************************************)
-(*   kind of global references                                         *)
-(***********************************************************************)
-
-type global_reference =
-  | ConstRef of section_path
-  | IndRef of inductive_path
-  | ConstructRef of constructor_path
-
 (**********************************************************************)
 (*          Non primitive term destructors                            *)
 (**********************************************************************)
@@ -1377,7 +1377,7 @@ let rel_list n m =
 
 (* Various occurs checks *)
 
-(* (occur_const (s:section_path) c) -> true if constant s occurs in c,
+(* (occur_const s c) -> true if constant s occurs in c,
  * false otherwise *)
 let occur_const s c = 
   let rec occur_rec c = match kind_of_term c with
@@ -1661,7 +1661,7 @@ type constr_operator =
   | OpSort of sorts
   | OpRel of int | OpVar of identifier
   | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
-  | OpApp | OpConst of section_path
+  | OpApp | OpConst of constant_path
   | OpEvar of existential_key
   | OpMutInd of inductive_path
   | OpMutConstruct of constructor_path
diff --git a/kernel/term.mli b/kernel/term.mli
index 5c9e5894ea..f909b90da8 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -31,6 +31,19 @@ type case_printing =
 (* the integer is the number of real args, needed for reduction *)
 type case_info = int array * case_printing
 
+(********************************************************************)
+(* type of global reference *)
+
+type global_reference =
+  | VarRef of section_path
+  | ConstRef of constant_path
+  | IndRef of inductive_path
+  | ConstructRef of constructor_path
+  | EvarRef of int
+
+(********************************************************************)
+(* The type of constructions *)
+
 type constr
 
 (* [types] is the same as [constr] but is intended to be used where a
@@ -57,13 +70,6 @@ type rel_declaration = name * constr option * types
 
 type arity = rel_declaration list * sorts
 
-(*i********************************************************************i*)
-(*s type of global reference *)
-type global_reference =
-  | ConstRef of section_path
-  | IndRef of inductive_path
-  | ConstructRef of constructor_path
-
 (*s Functions for dealing with constr terms.
   The following functions are intended to simplify and to uniform the 
   manipulation of terms. Some of these functions may be overlapped with
@@ -74,7 +80,7 @@ type global_reference =
 (* [constr array] is an instance matching definitional [named_context] in
    the same order (i.e. last argument first) *)
 type existential = int * constr array
-type constant = section_path * constr array
+type constant = constant_path * constr array
 type constructor = constructor_path * constr array
 type inductive = inductive_path * constr array
 type rec_declaration = constr array * name list * constr array
@@ -302,9 +308,9 @@ i*)
 val destApplication : constr -> constr * constr array
 
 (* Destructs a constant *)
-val destConst : constr -> section_path * constr array
+val destConst : constr -> constant_path * constr array
 val isConst : constr -> bool
-val path_of_const : constr -> section_path
+val path_of_const : constr -> constant_path
 val args_of_const : constr -> constr array
 
 (* Destructs an existential variable *)
@@ -492,7 +498,7 @@ val occur_existential : constr -> bool
 
 (* [(occur_const (s:section_path) c)] returns [true] if constant [s] occurs 
    in c, [false] otherwise *)
-val occur_const : section_path -> constr -> bool
+val occur_const : constant_path -> constr -> bool
 
 (* [(occur_evar ev c)] returns [true] if existential variable [ev] occurs 
    in c, [false] otherwise *)
@@ -537,7 +543,7 @@ type constr_operator =
   | OpSort of sorts
   | OpRel of int | OpVar of identifier
   | OpCast | OpProd of name | OpLambda of name | OpLetIn of name
-  | OpApp | OpConst of section_path
+  | OpApp | OpConst of constant_path
   | OpEvar of existential_key
   | OpMutInd of inductive_path
   | OpMutConstruct of constructor_path