From d44846131cf2fab2d3c45d435b84d802b1af8d43 Mon Sep 17 00:00:00 2001
From: herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Wed, 15 Dec 1999 15:24:13 +0000
Subject: Nouveaux types 'constructor' et 'inductive' dans Term; les fonctions
 sur les inductifs prennent maintenant des 'inductive' en paramètres; elle
 n'ont plus besoin de faire des appels dangereux aux find_m*type qui
 centralisent la levée de raise Induc.
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 toplevel/class.ml     |  6 +++---
 toplevel/command.ml   | 15 ++++++++-------
 toplevel/discharge.ml |  2 +-
 toplevel/himsg.ml     |  2 +-
 4 files changed, 13 insertions(+), 12 deletions(-)

(limited to 'toplevel')

diff --git a/toplevel/class.ml b/toplevel/class.ml
index 7912b2fdf..f8b84b7b6 100644
--- a/toplevel/class.ml
+++ b/toplevel/class.ml
@@ -117,10 +117,10 @@ let coe_constructor_at_head t =
   let rec aux t' =
     match kind_of_term t' with
       | IsConst (sp,l) -> (Array.to_list l),NAM_SP sp
-      | IsMutInd (sp,_,l) -> (Array.to_list l),NAM_SP sp
+      | IsMutInd ((sp,_),l) -> (Array.to_list l),NAM_SP sp
       | IsVar id  -> [],NAM_Var id
       | IsCast (c,_) -> aux c
-      | IsMutConstruct (sp,i,j,l) -> (Array.to_list l),NAM_Construct ((sp,i),j)
+      | IsMutConstruct (cstr_sp,l) -> (Array.to_list l),NAM_Construct cstr_sp
       | IsAppL(f,args) -> aux f
       |  _ -> raise Not_found
   in 
@@ -130,7 +130,7 @@ let constructor_at_head1 t =
   let rec aux t' =
     match kind_of_term t' with
       | IsConst (sp,l) -> t',[],(Array.to_list l),CL_SP sp,0
-      | IsMutInd (sp,i,l) -> t',[],(Array.to_list l),CL_IND (sp,i),0
+      | IsMutInd (ind_sp,l) -> t',[],(Array.to_list l),CL_IND ind_sp,0
       | IsVar id -> t',[],[],CL_Var id,0
       | IsCast (c,_) -> aux c
       | IsAppL(f,args) -> 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index c1860012b..ce804aa7f 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -337,15 +337,16 @@ let build_corecursive lnameardef =
   in
   ()
 
-exception NotInductive
 let inductive_of_ident id =
-  try match kind_of_term (global_reference CCI id) with
+  let c =
+    try global_reference CCI id
+    with Not_found ->
+      errorlabstrm "inductive_of_ident" ((string_of_id id) ^ " not found")
+  in
+  match kind_of_term (global_reference CCI id) with
     | IsMutInd ind -> ind
-    | _ -> raise NotInductive
-  with Not_found | NotInductive ->
-       errorlabstrm "inductive_of_ident"
-	 [< 'sTR (string_of_id id); 'sPC;
-	    'sTR "is not an inductive type" >]
+    | _ -> errorlabstrm "inductive_of_ident"
+	[< 'sTR (string_of_id id); 'sPC; 'sTR "is not an inductive type" >]
 
 let build_scheme lnamedepindsort = 
   let lrecnames = List.map (fun (f,_,_,_) -> f) lnamedepindsort
diff --git a/toplevel/discharge.ml b/toplevel/discharge.ml
index 15f52e412..f13890228 100644
--- a/toplevel/discharge.ml
+++ b/toplevel/discharge.ml
@@ -151,7 +151,7 @@ let process_inductive osecsp nsecsp oldenv (ids_to_discard,modlist) mib =
   let lmodif_one_mind i = 
     let nbc = Array.length (mind_nth_type_packet mib i).mind_consnames in 
     (MutInd(osecsp,i),DO_ABSTRACT(MutInd(nsecsp,i),modl))::
-    (MutCase(Some (osecsp,i)),DO_ABSTRACT(MutCase(Some (nsecsp,i)),[]))::
+    (MutCase(osecsp,i),DO_ABSTRACT(MutCase(nsecsp,i),[]))::
     (list_tabulate
        (function j -> 
 	  let j' = j + 1 in
diff --git a/toplevel/himsg.ml b/toplevel/himsg.ml
index a7cc960ab..78709719a 100644
--- a/toplevel/himsg.ml
+++ b/toplevel/himsg.ml
@@ -217,7 +217,7 @@ let explain_bad_constructor k ctx cstr ind =
      'sTR " in inductive type "; pt >]
 
 let explain_wrong_numarg_of_constructor k ctx cstr n =
-  let pc = pr_constructor cstr in
+  let pc = pr_constructor (cstr,[||]) in
   [<'sTR "The constructor "; pc;
     'sTR " expects " ; 'iNT n ; 'sTR " arguments. ">]
 
-- 
cgit v1.2.3