diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-15 15:24:13 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-12-15 15:24:13 +0000 |
| commit | d44846131cf2fab2d3c45d435b84d802b1af8d43 (patch) | |
| tree | 20de854b9ba4de7cbd01470559e956451a1d5d8e /toplevel | |
| parent | 490c8fa3145e861966dd83f6dc9478b0b96de470 (diff) | |
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.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@257 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'toplevel')
| -rw-r--r-- | toplevel/class.ml | 6 | ||||
| -rw-r--r-- | toplevel/command.ml | 15 | ||||
| -rw-r--r-- | toplevel/discharge.ml | 2 | ||||
| -rw-r--r-- | toplevel/himsg.ml | 2 |
4 files changed, 13 insertions, 12 deletions
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. ">] |