From f99150300603ce0d87db716efc52fa88967d4460 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 1 Dec 1999 23:13:01 +0000
Subject: 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
---
 kernel/term.ml | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'kernel/term.ml')

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. *)
 
-- 
cgit v1.2.3