diff options
| author |  Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2009-02-01 00:54:40 +0100 |
| commit | cfbfe13f5b515ae2e3c6cdd97e2ccee03bc26e56 (patch) | |
| tree | b7832bd5d412a5a5d69cb36ae2ded62c71124c22 /pretyping/indrec.ml | |
| parent | 113b703a695acbe31ac6dd6a8c4aa94f6fda7545 (diff) | |
Imported Upstream version 8.2~rc2+dfsgupstream/8.2.rc2+dfsg
Diffstat (limited to 'pretyping/indrec.ml')
| -rw-r--r-- | pretyping/indrec.ml | 15 |
1 files changed, 7 insertions, 8 deletions
diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index b4b8f0b8..d3123eb6 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: indrec.ml 11309 2008-08-06 10:30:35Z herbelin $ *) +(* $Id: indrec.ml 11735 2009-01-02 17:22:31Z herbelin $ *) open Pp open Util @@ -29,8 +29,7 @@ open Sign (* Errors related to recursors building *) type recursion_scheme_error = - | NotAllowedCaseAnalysis of bool * sorts * inductive - | BadInduction of bool * identifier * sorts + | NotAllowedCaseAnalysis of (*isrec:*) bool * sorts * inductive | NotMutualInScheme of inductive * inductive exception RecursionSchemeError of recursion_scheme_error @@ -57,8 +56,7 @@ let mis_make_case_com depopt env sigma ind (mib,mip as specif) kind = if not (List.mem kind (elim_sorts specif)) then raise (RecursionSchemeError - (NotAllowedCaseAnalysis - (dep,(new_sort_in_family kind),ind))); + (NotAllowedCaseAnalysis (false,new_sort_in_family kind,ind))); let ndepar = mip.mind_nrealargs + 1 in @@ -502,10 +500,10 @@ let instantiate_type_indrec_scheme sort npars term = let check_arities listdepkind = let _ = List.fold_left (fun ln ((_,ni as mind),mibi,mipi,dep,kind) -> - let id = mipi.mind_typename in let kelim = elim_sorts (mibi,mipi) in if not (List.exists ((=) kind) kelim) then raise - (RecursionSchemeError (BadInduction (dep,id,new_sort_in_family kind))) + (RecursionSchemeError + (NotAllowedCaseAnalysis (true,new_sort_in_family kind,mind))) else if List.mem ni ln then raise (RecursionSchemeError (NotMutualInScheme (mind,mind))) else ni::ln) @@ -593,7 +591,8 @@ let lookup_eliminator ind_sp s = errorlabstrm "default_elim" (strbrk "Cannot find the elimination combinator " ++ pr_id id ++ strbrk ", the elimination of the inductive definition " ++ - pr_id id ++ strbrk " on sort " ++ pr_sort_family s ++ + pr_global_env Idset.empty (IndRef ind_sp) ++ + strbrk " on sort " ++ pr_sort_family s ++ strbrk " is probably not allowed.") |