diff options
Diffstat (limited to 'library/indrec.ml')
| -rw-r--r-- | library/indrec.ml | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/library/indrec.ml b/library/indrec.ml index 251656c60..f15ed4b53 100644 --- a/library/indrec.ml +++ b/library/indrec.ml @@ -40,10 +40,11 @@ let mis_make_case_com depopt env sigma mispec kind = | None -> mis_sort mispec <> (Prop Null) | Some d -> d in - if not (List.exists (base_sort_cmp CONV kind) (mis_kelim mispec)) then + if not (List.exists ((=) kind) (mis_kelim mispec)) then raise (InductiveError - (NotAllowedCaseAnalysis (dep,kind,mis_inductive mispec))); + (NotAllowedCaseAnalysis + (dep,(sort_of_elimination kind),mis_inductive mispec))); let nbargsprod = mis_nrealargs mispec + 1 in @@ -74,7 +75,7 @@ let mis_make_case_com depopt env sigma mispec kind = mkLambda_string "f" t (add_branch (push_rel (Anonymous, None, t) env) (k+1)) in - let typP = make_arity env' dep indf kind in + let typP = make_arity env' dep indf (sort_of_elimination kind) in it_mkLambda_or_LetIn_name env (mkLambda_string "P" typP (add_branch (push_rel (Anonymous,None,typP) env') 0)) lnamespar @@ -371,7 +372,7 @@ let mis_make_indrec env sigma listdepkind mispec = let rec put_arity env i = function | (mispeci,dep,kinds)::rest -> let indf = make_ind_family (mispeci,extended_rel_list i lnamespar) in - let typP = make_arity env dep indf kinds in + let typP = make_arity env dep indf (sort_of_elimination kinds) in mkLambda_string "P" typP (put_arity (push_rel (Anonymous,None,typP) env) (i+1) rest) | [] -> @@ -432,11 +433,12 @@ let instanciate_indrec_scheme sort = let check_arities listdepkind = List.iter - (function (mispeci,dep,kinds) -> + (function (mispeci,dep,kind) -> let id = mis_typename mispeci in let kelim = mis_kelim mispeci in - if not (List.exists (base_sort_cmp CONV kinds) kelim) then - raise (InductiveError (BadInduction (dep, id, kinds)))) + if not (List.exists ((=) kind) kelim) then + raise + (InductiveError (BadInduction (dep, id, sort_of_elimination kind)))) listdepkind let build_mutual_indrec env sigma = function @@ -459,8 +461,8 @@ let build_mutual_indrec env sigma = function | _ -> anomaly "build_indrec expects a non empty list of inductive types" let build_indrec env sigma mispec = - let kind = mis_sort mispec in - let dep = kind <> Prop Null in + let kind = elimination_of_sort (mis_sort mispec) in + let dep = kind <> ElimOnProp in List.hd (mis_make_indrec env sigma [(mispec,dep,kind)] mispec) (**********************************************************************) |