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

1 files changed, 5 insertions, 5 deletions

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 *)