diff options
| -rw-r--r-- | CHANGES | 3 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 126 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 30 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/rewrite.ml4 | 2 | ||||
| -rw-r--r-- | tactics/tactics.ml | 116 | ||||
| -rw-r--r-- | tactics/tactics.mli | 4 | ||||
| -rw-r--r-- | tactics/tactics.mllib | 5 | ||||
| -rw-r--r-- | test-suite/success/apply.v | 34 | ||||
| -rw-r--r-- | toplevel/indschemes.ml | 108 |
10 files changed, 297 insertions, 135 deletions
@@ -48,6 +48,9 @@ Tactics avoided by unsetting option "Automatic Introduction"). - Made quantified hypotheses get the name they would have if introduced in the context (possible but rare source of incompatibilities). +- When applying a component of a conjunctive lemma, "apply in" (and + sequences of "apply in") now leave the side conditions of the lemmas + uniformly after the main goal (possible source of rare incompatibilities). Tactic Language diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml new file mode 100644 index 000000000..e3f29fe59 --- /dev/null +++ b/tactics/elimschemes.ml @@ -0,0 +1,126 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +(* Created by Hugo Herbelin from contents related to inductive schemes + initially developed by Christine Paulin (induction schemes), Vincent + Siles (decidable equality and boolean equality) and Matthieu Sozeau + (combined scheme) in file command.ml, Sep 2009 *) + +(* This file builds schemes related to case analysis and recursion schemes *) + +open Term +open Indrec +open Declarations +open Typeops +open Termops +open Ind_tables + +(* Induction/recursion schemes *) + +let optimize_non_type_induction_scheme kind dep sort ind = + if check_scheme kind ind then + (* in case the inductive has a type elimination, generates only one + induction scheme, the other ones share the same code with the + apropriate type *) + let cte = find_scheme kind ind in + let c = mkConst cte in + let t = type_of_constant (Global.env()) cte in + let (mib,mip) = Global.lookup_inductive ind in + let npars = + (* if a constructor of [ind] contains a recursive call, the scheme + is generalized only wrt recursively uniform parameters *) + if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) + then + mib.mind_nparams_rec + else + mib.mind_nparams in + snd (weaken_sort_scheme (new_sort_in_family sort) npars c t) + else + build_induction_scheme (Global.env()) Evd.empty ind dep sort + +let build_induction_scheme_in_type dep sort ind = + build_induction_scheme (Global.env()) Evd.empty ind dep sort + +let rect_scheme_kind_from_type = + declare_individual_scheme_object "_rect_nodep" + (build_induction_scheme_in_type false InType) + +let rect_scheme_kind_from_prop = + declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" + (build_induction_scheme_in_type false InType) + +let rect_dep_scheme_kind_from_type = + declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" + (build_induction_scheme_in_type true InType) + +let rect_dep_scheme_kind_from_prop = + declare_individual_scheme_object "_rect_dep" + (build_induction_scheme_in_type true InType) + +let ind_scheme_kind_from_type = + declare_individual_scheme_object "_ind_nodep" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) + +let ind_scheme_kind_from_prop = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" + (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) + +let ind_dep_scheme_kind_from_type = + declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" + (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) + +let ind_dep_scheme_kind_from_prop = + declare_individual_scheme_object "_ind_dep" + (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp) + +let rec_scheme_kind_from_type = + declare_individual_scheme_object "_rec_nodep" + (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) + +let rec_scheme_kind_from_prop = + declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" + (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) + +let rec_dep_scheme_kind_from_type = + declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" + (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) + +let rec_dep_scheme_kind_from_prop = + declare_individual_scheme_object "_rec_dep" + (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet) + +(* Case analysis *) + +let build_case_analysis_scheme_in_type dep sort ind = + build_case_analysis_scheme (Global.env()) Evd.empty ind dep sort + +let case_scheme_kind_from_type = + declare_individual_scheme_object "_case_nodep" + (build_case_analysis_scheme_in_type false InType) + +let case_scheme_kind_from_prop = + declare_individual_scheme_object "_case" ~aux:"_case_from_prop" + (build_case_analysis_scheme_in_type false InType) + +let case_dep_scheme_kind_from_type = + declare_individual_scheme_object "_case" ~aux:"_case_from_type" + (build_case_analysis_scheme_in_type true InType) + +let case_dep_scheme_kind_from_type_in_prop = + declare_individual_scheme_object "_casep_dep" + (build_case_analysis_scheme_in_type true InProp) + +let case_dep_scheme_kind_from_prop = + declare_individual_scheme_object "_case_dep" + (build_case_analysis_scheme_in_type true InType) + +let case_dep_scheme_kind_from_prop_in_prop = + declare_individual_scheme_object "_casep" + (build_case_analysis_scheme_in_type true InProp) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli new file mode 100644 index 000000000..fecf3e60d --- /dev/null +++ b/tactics/elimschemes.mli @@ -0,0 +1,30 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +(* $Id$ *) + +open Ind_tables + +(* Induction/recursion schemes *) + +val rect_scheme_kind_from_prop : individual scheme_kind +val ind_scheme_kind_from_prop : individual scheme_kind +val rec_scheme_kind_from_prop : individual scheme_kind +val rect_dep_scheme_kind_from_type : individual scheme_kind +val ind_dep_scheme_kind_from_type : individual scheme_kind +val rec_dep_scheme_kind_from_type : individual scheme_kind + + +(* Case analysis schemes *) + +val case_scheme_kind_from_type : individual scheme_kind +val case_scheme_kind_from_prop : individual scheme_kind +val case_dep_scheme_kind_from_type : individual scheme_kind +val case_dep_scheme_kind_from_type_in_prop : individual scheme_kind +val case_dep_scheme_kind_from_prop : individual scheme_kind +val case_dep_scheme_kind_from_prop_in_prop : individual scheme_kind diff --git a/tactics/equality.ml b/tactics/equality.ml index 86bb07829..c6c29a569 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1195,7 +1195,9 @@ let cutSubstInHyp_LR eqn id gls = let body,expected_goal = pf_apply subst_tuple_term gls e1 e2 idtyp in if not (dependent (mkRel 1) body) then raise NothingToRewrite; cut_replacing id expected_goal - (tclTHENFIRST (bareRevSubstInConcl lbeq body eq)) gls + (tclTHENFIRST + (bareRevSubstInConcl lbeq body eq) + (refine_no_check (mkVar id))) gls let cutSubstInHyp_RL eqn id gls = (tclTHENS (cutSubstInHyp_LR (swap_equands gls eqn) id) diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4 index 15ef2db2d..aea8c0ccf 100644 --- a/tactics/rewrite.ml4 +++ b/tactics/rewrite.ml4 @@ -860,7 +860,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat goal_meta clause gl = mkApp (mkLambda (Name (id_of_string "lemma"), ty, p), [| t |]) in cut_replacing id newt - (fun x -> Tacmach.refine_no_check (mkApp (term, [| mkVar id |]))) + (Tacmach.refine_no_check (mkApp (term, [| mkVar id |]))) | None -> (match abs with | None -> diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 24258bdfb..dc51c6d0c 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -94,6 +94,21 @@ let _ = optread = (fun () -> !dependent_propositions_elimination) ; optwrite = (fun b -> dependent_propositions_elimination := b) } +let apply_in_side_conditions_come_first = ref true + +let use_apply_in_side_conditions_come_first () = + !apply_in_side_conditions_come_first + && Flags.version_strictly_greater Flags.V8_2 + +let _ = + declare_bool_option + { optsync = true; + optname = "apply-in side-conditions coming first"; + optkey = ["Side";"Conditions";"First";"For";"apply";"in"]; + optread = (fun () -> !dependent_propositions_elimination) ; + optwrite = (fun b -> dependent_propositions_elimination := b) } + + (*********************************************) (* Tactics *) (*********************************************) @@ -646,11 +661,31 @@ let cut c gl = let cut_intro t = tclTHENFIRST (cut t) intro -(* cut_replacing échoue si l'hypothèse à remplacer apparaît dans le - but, ou dans une autre hypothèse *) -let cut_replacing id t tac = - tclTHENLAST (internal_cut_rev_replace id t) - (tac (refine_no_check (mkVar id))) +(* [assert_replacing id T tac] adds the subgoals of the proof of [T] + before the current goal + + id:T0 id:T0 id:T + ===== ------> tac(=====) + ==== + G T G + + It fails if the hypothesis to replace appears in the goal or in + another hypothesis. +*) + +let assert_replacing id t tac = tclTHENFIRST (internal_cut_replace id t) tac + +(* [cut_replacing id T tac] adds the subgoals of the proof of [T] + after the current goal + + id:T0 id:T id:T0 + ===== ------> ==== + tac(=====) + G G T + + It fails if the hypothesis to replace appears in the goal or in + another hypothesis. +*) + +let cut_replacing id t tac = tclTHENLAST (internal_cut_rev_replace id t) tac let cut_in_parallel l = let rec prec = function @@ -664,7 +699,13 @@ let error_uninstantiated_metas t clenv = let id = match na with Name id -> id | _ -> anomaly "unnamed dependent meta" in errorlabstrm "" (str "Cannot find an instance for " ++ pr_id id ++ str".") -let clenv_refine_in with_evars ?(with_classes=true) id clenv gl = +(* For a clenv expressing some lemma [C[?1:T1,...,?n:Tn] : P] and some + goal [G], [clenv_refine_in] returns [n+1] subgoals, the [n] last + ones (resp [n] first ones if [sidecond_first] is [true]) being the + [Ti] and the first one (resp last one) being [G] whose hypothesis + [id] is replaced by P using the proof given by [tac] *) + +let clenv_refine_in ?(sidecond_first=false) with_evars ?(with_classes=true) id clenv gl = let clenv = clenv_pose_dependent_evars with_evars clenv in let clenv = if with_classes then @@ -677,9 +718,8 @@ let clenv_refine_in with_evars ?(with_classes=true) id clenv gl = let new_hyp_prf = clenv_value clenv in tclTHEN (tclEVARS clenv.evd) - (cut_replacing id new_hyp_typ - (fun x gl -> refine_no_check new_hyp_prf gl)) gl - + ((if sidecond_first then assert_replacing else cut_replacing) + id new_hyp_typ (refine_no_check new_hyp_prf)) gl (********************************************) (* Elimination tactics *) @@ -848,15 +888,28 @@ let simplest_case c = general_case_analysis false (c,NoBindings) (* Apply a tactic below the products of the conclusion of a lemma *) -let descend_in_conjunctions with_evars tac exit c gl = +let get_named_case_analysis_scheme sidecond_first ind sort gl = + if sidecond_first then + pf_apply build_case_analysis_scheme_default gl ind sort + else + let (mib,mip) = Global.lookup_inductive ind in + let kind = inductive_sort_family mip in + let scheme = match kind, sort with + | InProp, InProp -> Elimschemes.case_dep_scheme_kind_from_prop_in_prop + | InProp, (InType | InSet) -> Elimschemes.case_dep_scheme_kind_from_prop + | _, InProp -> Elimschemes.case_dep_scheme_kind_from_type_in_prop + | _, (InType | InSet) -> Elimschemes.case_dep_scheme_kind_from_type + in mkConst (Ind_tables.find_scheme scheme ind) + +let descend_in_conjunctions sidecond_first with_evars tac exit c gl = try - let (mind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in + let (ind,t) = pf_reduce_to_quantified_ind gl (pf_type_of gl c) in match match_with_tuple (strip_prod t) with | Some (_,_,isrec) -> - let n = (mis_constr_nargs mind).(0) in + let n = (mis_constr_nargs ind).(0) in let sort = elimination_sort_of_goal gl in - let elim = pf_apply build_case_analysis_scheme_default gl mind sort in - tclTHENLAST + let elim = get_named_case_analysis_scheme sidecond_first ind sort gl in + (if sidecond_first then tclTHENLAST else tclTHENFIRST) (general_elim with_evars (c,NoBindings) {elimindex = None; elimbody = (elim,NoBindings)}) (tclTHENLIST [ @@ -928,7 +981,7 @@ let general_apply with_delta with_destruct with_evars (loc,(c,lbind)) gl0 = try if concl_nprod <> 0 then try_apply thm_ty 0 else raise Exit with PretypeError _|RefinerError _|UserError _|Failure _|Exit -> if with_destruct then - descend_in_conjunctions with_evars + descend_in_conjunctions true with_evars try_main_apply (fun _ -> Stdpp.raise_with_loc loc exn) c gl else Stdpp.raise_with_loc loc exn @@ -1001,7 +1054,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl = with NotExtensibleClause -> raise err in aux (make_clenv_binding gl (d,thm) lbind) -let apply_in_once with_delta with_destruct with_evars id +let apply_in_once sidecond_first with_delta with_destruct with_evars id (loc,((sigma,d),lbind)) gl0 = let flags = if with_delta then default_unify_flags else default_no_delta_unify_flags in @@ -1011,19 +1064,17 @@ let apply_in_once with_delta with_destruct with_evars id let rec aux with_destruct c gl = try let clause = apply_in_once_main flags innerclause (c,lbind) gl in - let res = clenv_refine_in with_evars id clause gl in + let res = clenv_refine_in ~sidecond_first with_evars id clause gl in if not with_evars then check_evars (fst res).sigma sigma gl0; res with exn when with_destruct -> - descend_in_conjunctions true aux (fun _ -> raise exn) c gl + descend_in_conjunctions sidecond_first true aux (fun _ -> raise exn) c gl in if sigma = Evd.empty then aux with_destruct d gl0 else tclTHEN (tclEVARS (Evd.merge gl0.sigma sigma)) (aux with_destruct d) gl0 - - (* A useful resolution tactic which, if c:A->B, transforms |- C into |- B -> C and |- A @@ -1424,16 +1475,29 @@ let as_tac id ipat = match ipat with user_err_loc (loc,"", str "Disjunctive/conjunctive pattern expected") | None -> tclIDTAC +let tclMAPLAST tacfun l = + List.fold_right (fun x -> tclTHENLAST (tacfun x)) l tclIDTAC + let tclMAPFIRST tacfun l = List.fold_right (fun x -> tclTHENFIRST (tacfun x)) l tclIDTAC -let general_apply_in with_delta with_destruct with_evars id lemmas ipat gl = - tclTHENFIRST (* Skip the side conditions of the applied lemma *) - (tclMAPFIRST (apply_in_once with_delta with_destruct with_evars id) lemmas) - (as_tac id ipat) - gl +let general_apply_in sidecond_first with_delta with_destruct with_evars + id lemmas ipat = + if sidecond_first then + (* Skip the side conditions of the applied lemma *) + tclTHENLAST + (tclMAPLAST + (apply_in_once sidecond_first with_delta with_destruct with_evars id) + lemmas) + (as_tac id ipat) + else + tclTHENFIRST + (tclMAPFIRST + (apply_in_once sidecond_first with_delta with_destruct with_evars id) + lemmas) + (as_tac id ipat) -let apply_in simple with_evars = general_apply_in simple simple with_evars +let apply_in simple with_evars = general_apply_in false simple simple with_evars let simple_apply_in id c = apply_in false false id [dloc,((Evd.empty,c),NoBindings)] None diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 2202fa8c8..b894628c3 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -359,8 +359,8 @@ val intros_transitivity : constr option -> tactic val cut : constr -> tactic val cut_intro : constr -> tactic -val cut_replacing : - identifier -> constr -> (tactic -> tactic) -> tactic +val assert_replacing : identifier -> types -> tactic -> tactic +val cut_replacing : identifier -> types -> tactic -> tactic val cut_in_parallel : constr list -> tactic val assert_as : bool -> intro_pattern_expr located option -> constr -> tactic diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib index 8c02e4662..0a634138a 100644 --- a/tactics/tactics.mllib +++ b/tactics/tactics.mllib @@ -4,13 +4,14 @@ Btermdn Nbtermdn Tacticals Hipattern +Ind_tables +Eqschemes +Elimschemes Tactics Hiddentac Elim Dhyp Auto -Ind_tables -Eqschemes Equality Contradiction Inv diff --git a/test-suite/success/apply.v b/test-suite/success/apply.v index 7f0041714..45da9593c 100644 --- a/test-suite/success/apply.v +++ b/test-suite/success/apply.v @@ -297,13 +297,37 @@ reflexivity. exact I. Qed. -(* Check chaining of "apply in" on the last subgoal (assuming that - side conditions come first) *) +(* Check that "apply" is chained on the last subgoal of each lemma and + that side conditions come first (as it is the case since 8.2) *) -Lemma chaining : - forall B C D : Prop, (True -> B -> C) -> (C -> D) -> B -> D. +Lemma chaining : + forall A B C : Prop, + (1=1 -> (2=2 -> A -> B) /\ True) -> + (3=3 -> (True /\ (4=4 -> C -> A))) -> C -> B. Proof. intros. -apply H, H0 in H1; auto. +apply H, H0. +exact (refl_equal 1). +exact (refl_equal 2). +exact (refl_equal 3). +exact (refl_equal 4). +assumption. Qed. +(* Check that the side conditions of "apply in", even when chained and + used through conjunctions, come last (as it is the case for single + calls to "apply in" w/o destruction of conjunction since 8.2) *) + +Lemma chaining_in : + forall A B C : Prop, + (1=1 -> True /\ (B -> 2=2 -> 5=0)) -> + (3=3 -> (A -> 4=4 -> B) /\ True) -> A -> 0=5. +Proof. +intros. +apply H0, H in H1 as ->. +exact (refl_equal 0). +exact (refl_equal 1). +exact (refl_equal 2). +exact (refl_equal 3). +exact (refl_equal 4). +Qed. diff --git a/toplevel/indschemes.ml b/toplevel/indschemes.ml index abf53fd97..3c0647112 100644 --- a/toplevel/indschemes.ml +++ b/toplevel/indschemes.ml @@ -41,6 +41,7 @@ open Vernacexpr open Ind_tables open Auto_ind_decl open Eqschemes +open Elimschemes (* Flags governing automatic synthesis of schemes *) @@ -173,79 +174,20 @@ let try_declare_beq_scheme kn = let declare_beq_scheme = declare_beq_scheme_with [] -(* Induction/recursion schemes *) +(* Case analysis schemes *) -let optimize_non_type_induction_scheme kind dep sort ind = - if check_scheme kind ind then +let declare_one_case_analysis_scheme ind = + let (mib,mip) = Global.lookup_inductive ind in + let kind = inductive_sort_family mip in + let dep = if kind = InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in + let kelim = elim_sorts (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 apropriate type *) - let cte = find_scheme kind ind in - let c = mkConst cte in - let t = type_of_constant (Global.env()) cte in - let (mib,mip) = Global.lookup_inductive ind in - let npars = - (* if a constructor of [ind] contains a recursive call, the scheme - is generalized only wrt recursively uniform parameters *) - if (Inductiveops.mis_is_recursive_subset [snd ind] mip.mind_recargs) - then - mib.mind_nparams_rec - else - mib.mind_nparams in - snd (weaken_sort_scheme (new_sort_in_family sort) npars c t) - else - build_induction_scheme (Global.env()) Evd.empty ind dep sort - -let build_induction_scheme_in_type dep sort ind = - build_induction_scheme (Global.env()) Evd.empty ind dep sort - -let rect_scheme_kind_from_type = - declare_individual_scheme_object "_rect_nodep" - (build_induction_scheme_in_type false InType) - -let rect_scheme_kind_from_prop = - declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (build_induction_scheme_in_type false InType) - -let rect_dep_scheme_kind_from_type = - declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (build_induction_scheme_in_type true InType) - -let rect_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_rect_dep" - (build_induction_scheme_in_type true InType) - -let ind_scheme_kind_from_type = - declare_individual_scheme_object "_ind_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InProp) - -let ind_scheme_kind_from_prop = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" - (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InProp) - -let ind_dep_scheme_kind_from_type = - declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InProp) - -let ind_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_ind_dep" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InProp) - -let rec_scheme_kind_from_type = - declare_individual_scheme_object "_rec_nodep" - (optimize_non_type_induction_scheme rect_scheme_kind_from_type false InSet) - -let rec_scheme_kind_from_prop = - declare_individual_scheme_object "_rec" ~aux:"_rec_from_prop" - (optimize_non_type_induction_scheme rect_scheme_kind_from_prop false InSet) - -let rec_dep_scheme_kind_from_type = - declare_individual_scheme_object "_rec" ~aux:"_rec_from_type" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_type true InSet) + if List.mem InType kelim then + ignore (define_individual_scheme dep true None ind) -let rec_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_rec_dep" - (optimize_non_type_induction_scheme rect_dep_scheme_kind_from_prop true InSet) +(* Induction/recursion schemes *) let kinds_from_prop = [InType,rect_scheme_kind_from_prop; @@ -269,36 +211,6 @@ let declare_one_induction_scheme ind = List.iter (fun kind -> ignore (define_individual_scheme kind true None ind)) elims -let build_case_analysis_scheme_in_type dep ind = - build_case_analysis_scheme (Global.env()) Evd.empty ind dep InType - -let case_scheme_kind_from_type = - declare_individual_scheme_object "_case_nodep" - (build_case_analysis_scheme_in_type false) - -let case_scheme_kind_from_prop = - declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (build_case_analysis_scheme_in_type false) - -let case_dep_scheme_kind_from_type = - declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (build_case_analysis_scheme_in_type true) - -let case_dep_scheme_kind_from_prop = - declare_individual_scheme_object "_case_dep" - (build_case_analysis_scheme_in_type true) - -let declare_one_case_analysis_scheme ind = - let (mib,mip) = Global.lookup_inductive ind in - let kind = inductive_sort_family mip in - let dep = if kind = InProp then case_scheme_kind_from_prop else case_dep_scheme_kind_from_type in - let kelim = elim_sorts (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 - apropriate type *) - if List.mem InType kelim then - ignore (define_individual_scheme dep true None ind) - let declare_induction_schemes kn = let mib = Global.lookup_mind kn in if mib.mind_finite then begin |