diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/auto_ind_decl.ml | 4 | ||||
| -rw-r--r-- | vernac/himsg.ml | 1 | ||||
| -rw-r--r-- | vernac/indschemes.ml | 11 | ||||
| -rw-r--r-- | vernac/obligations.ml | 8 |
4 files changed, 13 insertions, 11 deletions
diff --git a/vernac/auto_ind_decl.ml b/vernac/auto_ind_decl.ml index 528829f3a5..5aec5cac2c 100644 --- a/vernac/auto_ind_decl.ml +++ b/vernac/auto_ind_decl.ml @@ -331,8 +331,8 @@ let build_beq_scheme mode kn = eff := Safe_typing.concat_private eff' !eff done; (Array.init nb_ind (fun i -> - let kelim = Inductive.elim_sorts (mib,mib.mind_packets.(i)) in - if not (Sorts.List.mem InSet kelim) then + let kelim = Inductive.elim_sort (mib,mib.mind_packets.(i)) in + if not (Sorts.family_leq InSet kelim) then raise (NonSingletonProp (kn,i)); let fix = match mib.mind_finite with | CoFinite -> diff --git a/vernac/himsg.ml b/vernac/himsg.ml index b2382ce6fc..a1f7835cbe 100644 --- a/vernac/himsg.ml +++ b/vernac/himsg.ml @@ -219,6 +219,7 @@ let explain_elim_arity env sigma ind c pj okinds = let pc = pr_leconstr_env env sigma c in let msg = match okinds with | Some(sorts,kp,ki,explanation) -> + let sorts = Inductiveops.sorts_below sorts in let pki = Sorts.pr_sort_family ki in let pkp = Sorts.pr_sort_family kp in let explanation = match explanation with diff --git a/vernac/indschemes.ml b/vernac/indschemes.ml index 6ac259b1fe..de7d2fd49a 100644 --- a/vernac/indschemes.ml +++ b/vernac/indschemes.ml @@ -216,11 +216,11 @@ let declare_one_case_analysis_scheme ind = else if not (Inductiveops.has_dependent_elim mib) then case_scheme_kind_from_type else case_dep_scheme_kind_from_type in - let kelim = elim_sorts (mib,mip) in + let kelim = elim_sort (mib,mip) in (* in case the inductive has a type elimination, generates only one induction scheme, the other ones share the same code with the appropriate type *) - if Sorts.List.mem InType kelim then + if Sorts.family_leq InType kelim then ignore (define_individual_scheme dep UserAutomaticRequest None ind) (* Induction/recursion schemes *) @@ -248,16 +248,17 @@ let declare_one_induction_scheme ind = let kind = inductive_sort_family mip in let from_prop = kind == InProp in let depelim = Inductiveops.has_dependent_elim mib in - let kelim = elim_sorts (mib,mip) in + let kelim = Inductiveops.sorts_below (elim_sort (mib,mip)) in let kelim = if Global.sprop_allowed () then kelim else List.filter (fun s -> s <> InSProp) kelim in let elims = List.map_filter (fun (sort,kind) -> - if Sorts.List.mem sort kelim then Some kind else None) + if List.mem_f Sorts.family_equal sort kelim then Some kind else None) (if from_prop then kinds_from_prop else if depelim then kinds_from_type - else nondep_kinds_from_type) in + else nondep_kinds_from_type) + in List.iter (fun kind -> ignore (define_individual_scheme kind UserAutomaticRequest None ind)) elims diff --git a/vernac/obligations.ml b/vernac/obligations.ml index ad175511b9..bc741a0ec7 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -820,8 +820,8 @@ let solve_by_tac ?loc name evi t poly ctx = Pfedit.build_constant_by_tactic id ~goal_kind:(goal_kind poly) ctx evi.evar_hyps evi.evar_concl t in let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in - let body, () = Future.force entry.const_entry_body in + let body = Future.force entry.const_entry_body in + let body = Safe_typing.inline_private_constants env body in let ctx' = Evd.merge_context_set ~sideff:true Evd.univ_rigid (Evd.from_ctx ctx') (snd body) in Inductiveops.control_only_guard env ctx' (EConstr.of_constr (fst body)); Some (fst body, entry.const_entry_type, Evd.evar_universe_context ctx') @@ -844,9 +844,9 @@ let obligation_terminator ?hook name num guard auto pf = | Admitted _ -> apply_terminator term pf | Proved (opq, id, { entries=[entry]; universes=uctx } ) -> begin let env = Global.env () in - let entry = Safe_typing.inline_private_constants_in_definition_entry env entry in let ty = entry.Entries.const_entry_type in - let (body, cstr), () = Future.force entry.Entries.const_entry_body in + let body = Future.force entry.const_entry_body in + let (body, cstr) = Safe_typing.inline_private_constants env body in let sigma = Evd.from_ctx uctx in let sigma = Evd.merge_context_set ~sideff:true Evd.univ_rigid sigma cstr in Inductiveops.control_only_guard (Global.env ()) sigma (EConstr.of_constr body); |