Intégration du Termast et du Retyping de HH, et modifications connexes

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

7 files changed, 22 insertions, 14 deletions

diff --git a/kernel/names.ml b/kernel/names.ml
index 316e0735a9..e04a41f42b 100644
--- a/kernel/names.ml
+++ b/kernel/names.ml
@@ -224,6 +224,11 @@ module Spset = Set.Make(SpOrdered)
 
 module Spmap = Map.Make(SpOrdered)
 
+(* Special references for inductive objects *)
+
+type inductive_path = section_path * int
+type constructor_path = inductive_path * int
+
 (* Hash-consing of name objects *)
 module Hident = Hashcons.Make(
   struct 
diff --git a/kernel/names.mli b/kernel/names.mli
index 541e4f61a6..b3f5811e4c 100644
--- a/kernel/names.mli
+++ b/kernel/names.mli
@@ -70,6 +70,9 @@ val sp_gt : section_path * section_path -> bool
 module Spset : Set.S with type elt = section_path
 module Spmap : Map.S with type key = section_path
 
+type inductive_path = section_path * int
+type constructor_path = inductive_path * int
+
 (* Hash-consing *)
 val hcons_names : unit ->
   (section_path -> section_path) * (section_path -> section_path) *
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 04d63da8ff..8f1ad37874 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -89,10 +89,10 @@ let rec execute mf env cstr =
 	(make_judge cofix larv.(i), cst)
 	  
     | IsSort (Prop c) -> 
-	(make_judge_of_prop_contents c, cst0)
+	(judge_of_prop_contents c, cst0)
 
     | IsSort (Type u) ->
-	make_judge_of_type u
+	judge_of_type u
 	  
     | IsAppL (f,args) ->
 	let (j,cst1) = execute mf env f in
diff --git a/kernel/term.ml b/kernel/term.ml
index 1a5c74e682..38dbc37655 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -20,8 +20,8 @@ type 'a oper =
   (* DOPN *)
   | AppL | Const of section_path | Abst of section_path
   | Evar of int
-  | MutInd of section_path * int
-  | MutConstruct of (section_path * int) * int
+  | MutInd of inductive_path
+  | MutConstruct of constructor_path
   | MutCase of case_info
   | Fix of int array * int
   | CoFix of int
@@ -30,7 +30,7 @@ type 'a oper =
       (* an extra slot, for putting in whatever sort of
          operator we need for whatever sort of application *)
 
-and case_info = (section_path * int) option
+and case_info = inductive_path option
 
 (* Sorts. *)
 
diff --git a/kernel/term.mli b/kernel/term.mli
index b849258606..6e7101ad34 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -17,14 +17,14 @@ type 'a oper =
   | Cast | Prod | Lambda
   | AppL | Const of section_path | Abst of section_path
   | Evar of int
-  | MutInd of section_path * int
-  | MutConstruct of (section_path * int) * int
+  | MutInd of inductive_path
+  | MutConstruct of constructor_path
   | MutCase of case_info
   | Fix of int array * int
   | CoFix of int
   | XTRA of string
 
-and case_info = (section_path * int) option
+and case_info = inductive_path option
 
 (*s The sorts of CCI. *)
 
@@ -287,13 +287,13 @@ val args_of_abst : constr -> constr array
 
 (* Destructs a (co)inductive type *)
 val destMutInd : constr -> section_path * int * constr array
-val op_of_mind : constr -> section_path * int
+val op_of_mind : constr -> inductive_path
 val args_of_mind : constr -> constr array
 val ci_of_mind : constr -> case_info
 
 (* Destructs a constructor *)
 val destMutConstruct : constr -> section_path * int * int * constr array
-val op_of_mconstr : constr -> (section_path * int) * int
+val op_of_mconstr : constr -> constructor_path
 val args_of_mconstr : constr -> constr array
 
 (* Destructs a term <p>Case c of lc1 | lc2 .. | lcn end *)
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 0824c192cf..7066462452 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -357,13 +357,13 @@ let judge_of_set =
     uj_type = DOP0(Sort type_0);
     uj_kind = DOP0(Sort type_1) }
 
-let make_judge_of_prop_contents = function
+let judge_of_prop_contents = function
   | Null -> judge_of_prop
   | Pos -> judge_of_set
 
 (* Type of Type(i). *)
 
-let make_judge_of_type u =
+let judge_of_type u =
   let (uu,uuu,c) = super_super u in
   { uj_val = DOP0 (Sort (Type u));
     uj_type = DOP0 (Sort (Type uu));
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index b935efd8c6..a271dc9ecb 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -42,9 +42,9 @@ val type_case_branches :
   env -> 'a evar_map -> constr -> constr -> constr -> constr 
     -> constr * constr array * constr 
 
-val make_judge_of_prop_contents : contents -> unsafe_judgment
+val judge_of_prop_contents : contents -> unsafe_judgment
 
-val make_judge_of_type : universe -> unsafe_judgment * constraints
+val judge_of_type : universe -> unsafe_judgment * constraints
 
 val abs_rel : 
   env -> 'a evar_map -> name -> typed_type -> unsafe_judgment