diff options
Diffstat (limited to 'pretyping')
| -rw-r--r-- | pretyping/cases.ml | 1 | ||||
| -rw-r--r-- | pretyping/indrec.ml | 22 | ||||
| -rw-r--r-- | pretyping/tacred.ml | 8 | ||||
| -rw-r--r-- | pretyping/tacred.mli | 5 |
4 files changed, 28 insertions, 8 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml index b56d5947ce..2b0a2dda95 100644 --- a/pretyping/cases.ml +++ b/pretyping/cases.ml @@ -1298,6 +1298,7 @@ and match_current pb (initial,tomatch) = compile_all_variables initial tomatch pb | IsInd (_,(IndType(indf,realargs) as indt),names) -> let mind,_ = dest_ind_family indf in + let mind = Tacred.check_privacy pb.env mind in let cstrs = get_constructors pb.env indf in let arsign, _ = get_arity pb.env indf in let eqns,onlydflt = group_equations pb (fst mind) current cstrs pb.mat in diff --git a/pretyping/indrec.ml b/pretyping/indrec.ml index 35a9cbdb22..bed77e6223 100644 --- a/pretyping/indrec.ml +++ b/pretyping/indrec.ml @@ -45,6 +45,15 @@ let mkLambda_string s t c = mkLambda (Name (Id.of_string s), t, c) (* Building curryfied elimination *) (*******************************************) +let is_private mib = + match mib.mind_private with + | Some true -> true + | _ -> false + +let check_privacy_block mib = + if is_private mib then + errorlabstrm ""(str"case analysis on a private inductive type") + (**********************************************************************) (* Building case analysis schemes *) (* Christine Paulin, 1996 *) @@ -54,12 +63,13 @@ let mis_make_case_com dep env sigma (ind, u as pind) (mib,mip as specif) kind = let lnamespar = Vars.subst_univs_context usubst mib.mind_params_ctxt in - - if not (Sorts.List.mem kind (elim_sorts specif)) then - raise - (RecursionSchemeError - (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))); - + let () = check_privacy_block mib in + let () = + if not (Sorts.List.mem kind (elim_sorts specif)) then + raise + (RecursionSchemeError + (NotAllowedCaseAnalysis (false, fst (Universes.fresh_sort_in_family env kind), pind))) + in let ndepar = mip.mind_nrealargs_ctxt + 1 in (* Pas génant car env ne sert pas à typer mais juste à renommer les Anonym *) diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index da45952548..383d233069 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -1093,6 +1093,10 @@ let pattern_occs loccs_trm env sigma c = (* Used in several tactics. *) +let check_privacy env ind = + if (fst (Inductive.lookup_mind_specif env (fst ind))).Declarations.mind_private = Some true then + errorlabstrm "" (str "case analysis on a private type") + else ind (* put t as t'=(x1:A1)..(xn:An)B with B an inductive definition of name name return name, B and t' *) @@ -1100,7 +1104,7 @@ let reduce_to_ind_gen allow_product env sigma t = let rec elimrec env t l = let t = hnf_constr env sigma t in match kind_of_term (fst (decompose_app t)) with - | Ind ind-> (ind, it_mkProd_or_LetIn t l) + | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t l) | Prod (n,ty,t') -> if allow_product then elimrec (push_rel (n,None,ty) env) t' ((n,None,ty)::l) @@ -1111,7 +1115,7 @@ let reduce_to_ind_gen allow_product env sigma t = was partially the case between V5.10 and V8.1 *) let t' = whd_betadeltaiota env sigma t in match kind_of_term (fst (decompose_app t')) with - | Ind ind-> (ind, it_mkProd_or_LetIn t' l) + | Ind ind-> (check_privacy env ind, it_mkProd_or_LetIn t' l) | _ -> errorlabstrm "" (str"Not an inductive product.") in elimrec env t [] diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 5146cd3458..5e4bc5c461 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -14,6 +14,7 @@ open Reductionops open Pattern open Globnames open Locus +open Univ type reduction_tactic_error = InvalidAbstraction of env * constr * (env * Type_errors.type_error) @@ -106,3 +107,7 @@ val contextually : bool -> occurrences * constr_pattern -> val e_contextually : bool -> occurrences * constr_pattern -> (patvar_map -> e_reduction_function) -> e_reduction_function + +(** Returns the same inductive if it is allowed for pattern-matching + raises an error otherwise. **) +val check_privacy : env -> inductive puniverses -> inductive puniverses |