diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/abstract.ml | 9 | ||||
| -rw-r--r-- | tactics/elimschemes.ml | 40 | ||||
| -rw-r--r-- | tactics/elimschemes.mli | 3 | ||||
| -rw-r--r-- | tactics/eqschemes.ml | 16 | ||||
| -rw-r--r-- | tactics/eqschemes.mli | 4 | ||||
| -rw-r--r-- | tactics/equality.ml | 55 | ||||
| -rw-r--r-- | tactics/hints.ml | 2 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 16 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 10 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 8 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 9 |
11 files changed, 82 insertions, 90 deletions
diff --git a/tactics/abstract.ml b/tactics/abstract.ml index a5b2f99457..967b0ef418 100644 --- a/tactics/abstract.ml +++ b/tactics/abstract.ml @@ -103,8 +103,8 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = question, how does abstract behave when discharge is local for example? *) let goal_kind, suffix = if opaque - then (Global,poly,Proof Theorem), "_subproof" - else (Global,poly,DefinitionBody Definition), "_subterm" in + then (Global ImportDefaultBehavior,poly,Proof Theorem), "_subproof" + else (Global ImportDefaultBehavior,poly,DefinitionBody Definition), "_subterm" in let id, goal_kind = name_op_to_name ~name_op ~name ~goal_kind suffix in Proofview.Goal.enter begin fun gl -> let env = Proofview.Goal.env gl in @@ -158,7 +158,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = (* do not compute the implicit arguments, it may be costly *) let () = Impargs.make_implicit_args false in (* ppedrot: seems legit to have abstracted subproofs as local*) - Declare.declare_private_constant ~role:Entries.Subproof ~internal:Declare.InternalTacticRequest ~local:true id decl + Declare.declare_private_constant ~internal:Declare.InternalTacticRequest ~local:ImportNeedQualified id decl in let cst, eff = Impargs.with_implicit_protection cst () in let inst = match const.Entries.const_entry_universes with @@ -173,8 +173,7 @@ let cache_term_by_tactic_then ~opaque ~name_op ?(goal_type=None) tac tacK = in let lem = mkConstU (cst, inst) in let evd = Evd.set_universe_context evd ectx in - let open Safe_typing in - let effs = concat_private eff + let effs = Evd.concat_side_effects eff Entries.(snd (Future.force const.const_entry_body)) in let solve = Proofview.tclEFFECTS effs <*> diff --git a/tactics/elimschemes.ml b/tactics/elimschemes.ml index 1170c1acd0..06449c38a8 100644 --- a/tactics/elimschemes.ml +++ b/tactics/elimschemes.ml @@ -51,7 +51,7 @@ let optimize_non_type_induction_scheme kind dep sort _ ind = else let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in - (c, Evd.evar_universe_context sigma), Safe_typing.empty_private_constants + (c, Evd.evar_universe_context sigma), Evd.empty_side_effects let build_induction_scheme_in_type dep sort ind = let env = Global.env () in @@ -59,18 +59,18 @@ let build_induction_scheme_in_type dep sort ind = let sigma, pind = Evd.fresh_inductive_instance env sigma ind in let sigma, c = build_induction_scheme env sigma pind dep sort in c, Evd.evar_universe_context sigma - + let rect_scheme_kind_from_type = declare_individual_scheme_object "_rect_nodep" - (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects) let rect_scheme_kind_from_prop = declare_individual_scheme_object "_rect" ~aux:"_rect_from_prop" - (fun _ x -> build_induction_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InType x, Evd.empty_side_effects) let rect_dep_scheme_kind_from_type = declare_individual_scheme_object "_rect" ~aux:"_rect_from_type" - (fun _ x -> build_induction_scheme_in_type true InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type true InType x, Evd.empty_side_effects) let rec_scheme_kind_from_type = declare_individual_scheme_object "_rec_nodep" ~aux:"_rec_nodep_from_type" @@ -90,7 +90,7 @@ let ind_scheme_kind_from_type = let sind_scheme_kind_from_type = declare_individual_scheme_object "_sind_nodep" - (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects) let ind_dep_scheme_kind_from_type = declare_individual_scheme_object "_ind" ~aux:"_ind_from_type" @@ -98,7 +98,7 @@ let ind_dep_scheme_kind_from_type = let sind_dep_scheme_kind_from_type = declare_individual_scheme_object "_sind" ~aux:"_sind_from_type" - (fun _ x -> build_induction_scheme_in_type true InSProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_induction_scheme_in_type true InSProp x, Evd.empty_side_effects) let ind_scheme_kind_from_prop = declare_individual_scheme_object "_ind" ~aux:"_ind_from_prop" @@ -106,8 +106,18 @@ let ind_scheme_kind_from_prop = let sind_scheme_kind_from_prop = declare_individual_scheme_object "_sind" ~aux:"_sind_from_prop" - (fun _ x -> build_induction_scheme_in_type false InSProp x, Safe_typing.empty_private_constants) - + (fun _ x -> build_induction_scheme_in_type false InSProp x, Evd.empty_side_effects) + +let nondep_elim_scheme from_kind to_kind = + match from_kind, to_kind with + | InProp, InProp -> ind_scheme_kind_from_prop + | InProp, InSProp -> sind_scheme_kind_from_prop + | InProp, InSet -> rec_scheme_kind_from_prop + | InProp, InType -> rect_scheme_kind_from_prop + | _ , InProp -> ind_scheme_kind_from_type + | _ , InSProp -> sind_scheme_kind_from_type + | _ , InSet -> rec_scheme_kind_from_type + | _ , InType -> rect_scheme_kind_from_type (* Case analysis *) @@ -120,24 +130,24 @@ let build_case_analysis_scheme_in_type dep sort ind = let case_scheme_kind_from_type = declare_individual_scheme_object "_case_nodep" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects) let case_scheme_kind_from_prop = declare_individual_scheme_object "_case" ~aux:"_case_from_prop" - (fun _ x -> build_case_analysis_scheme_in_type false InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type false InType x, Evd.empty_side_effects) let case_dep_scheme_kind_from_type = declare_individual_scheme_object "_case" ~aux:"_case_from_type" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects) let case_dep_scheme_kind_from_type_in_prop = declare_individual_scheme_object "_casep_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects) let case_dep_scheme_kind_from_prop = declare_individual_scheme_object "_case_dep" - (fun _ x -> build_case_analysis_scheme_in_type true InType x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InType x, Evd.empty_side_effects) let case_dep_scheme_kind_from_prop_in_prop = declare_individual_scheme_object "_casep" - (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Safe_typing.empty_private_constants) + (fun _ x -> build_case_analysis_scheme_in_type true InProp x, Evd.empty_side_effects) diff --git a/tactics/elimschemes.mli b/tactics/elimschemes.mli index 4472792449..2b8a053cc0 100644 --- a/tactics/elimschemes.mli +++ b/tactics/elimschemes.mli @@ -18,7 +18,7 @@ val optimize_non_type_induction_scheme : Sorts.family -> 'b -> Names.inductive -> - (Constr.constr * UState.t) * Safe_typing.private_constants + (Constr.constr * UState.t) * Evd.side_effects val rect_scheme_kind_from_prop : individual scheme_kind val ind_scheme_kind_from_prop : individual scheme_kind @@ -33,6 +33,7 @@ val sind_dep_scheme_kind_from_type : individual scheme_kind val rec_scheme_kind_from_type : individual scheme_kind val rec_dep_scheme_kind_from_type : individual scheme_kind +val nondep_elim_scheme : Sorts.family -> Sorts.family -> individual scheme_kind (** Case analysis schemes *) diff --git a/tactics/eqschemes.ml b/tactics/eqschemes.ml index 3fdd97616f..d66ae9cb24 100644 --- a/tactics/eqschemes.ml +++ b/tactics/eqschemes.ml @@ -229,7 +229,7 @@ let sym_scheme_kind = declare_individual_scheme_object "_sym_internal" (fun _ ind -> let c, ctx = build_sym_scheme (Global.env() (* side-effect! *)) ind in - (c, ctx), Safe_typing.empty_private_constants) + (c, ctx), Evd.empty_side_effects) (**********************************************************************) (* Build the involutivity of symmetry for an inductive type *) @@ -455,7 +455,7 @@ let build_l2r_rew_scheme dep env ind kind = else main_body)))))) in (c, UState.of_context_set ctx), - Safe_typing.concat_private eff' eff + Evd.concat_side_effects eff' eff (**********************************************************************) (* Build the left-to-right rewriting lemma for hypotheses associated *) @@ -708,7 +708,7 @@ let rew_l2r_dep_scheme_kind = (**********************************************************************) let rew_r2l_dep_scheme_kind = declare_individual_scheme_object "_rew_dep" - (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) + (fun _ ind -> build_r2l_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) (**********************************************************************) (* Dependent rewrite from right-to-left in hypotheses *) @@ -718,7 +718,7 @@ let rew_r2l_dep_scheme_kind = (**********************************************************************) let rew_r2l_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_dep" - (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) + (fun _ ind -> build_r2l_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) (**********************************************************************) (* Dependent rewrite from left-to-right in hypotheses *) @@ -728,7 +728,7 @@ let rew_r2l_forward_dep_scheme_kind = (**********************************************************************) let rew_l2r_forward_dep_scheme_kind = declare_individual_scheme_object "_rew_fwd_r_dep" - (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Safe_typing.empty_private_constants) + (fun _ ind -> build_l2r_forward_rew_scheme true (Global.env()) ind InType,Evd.empty_side_effects) (**********************************************************************) (* Non-dependent rewrite from either left-to-right in conclusion or *) @@ -742,7 +742,7 @@ let rew_l2r_forward_dep_scheme_kind = let rew_l2r_scheme_kind = declare_individual_scheme_object "_rew_r" (fun _ ind -> fix_r2l_forward_rew_scheme - (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Safe_typing.empty_private_constants) + (build_r2l_forward_rew_scheme false (Global.env()) ind InType), Evd.empty_side_effects) (**********************************************************************) (* Non-dependent rewrite from either right-to-left in conclusion or *) @@ -752,7 +752,7 @@ let rew_l2r_scheme_kind = (**********************************************************************) let rew_r2l_scheme_kind = declare_individual_scheme_object "_rew" - (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Safe_typing.empty_private_constants) + (fun _ ind -> build_r2l_rew_scheme false (Global.env()) ind InType, Evd.empty_side_effects) (* End of rewriting schemes *) @@ -836,4 +836,4 @@ let congr_scheme_kind = declare_individual_scheme_object "_congr" (fun _ ind -> (* May fail if equality is not defined *) build_congr (Global.env()) (get_coq_eq Univ.ContextSet.empty) ind, - Safe_typing.empty_private_constants) + Evd.empty_side_effects) diff --git a/tactics/eqschemes.mli b/tactics/eqschemes.mli index 4749aebd96..c15fa146d4 100644 --- a/tactics/eqschemes.mli +++ b/tactics/eqschemes.mli @@ -27,7 +27,7 @@ val rew_r2l_scheme_kind : individual scheme_kind val build_r2l_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_rew_scheme : bool -> env -> inductive -> Sorts.family -> - constr Evd.in_evar_universe_context * Safe_typing.private_constants + constr Evd.in_evar_universe_context * Evd.side_effects val build_r2l_forward_rew_scheme : bool -> env -> inductive -> Sorts.family -> constr Evd.in_evar_universe_context val build_l2r_forward_rew_scheme : @@ -39,7 +39,7 @@ val build_sym_scheme : env -> inductive -> constr Evd.in_evar_universe_context val sym_scheme_kind : individual scheme_kind val build_sym_involutive_scheme : env -> inductive -> - constr Evd.in_evar_universe_context * Safe_typing.private_constants + constr Evd.in_evar_universe_context * Evd.side_effects val sym_involutive_scheme_kind : individual scheme_kind (** Builds a congruence scheme for an equality type *) diff --git a/tactics/equality.ml b/tactics/equality.ml index 51eee2a053..ec0876110b 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -352,35 +352,35 @@ let find_elim hdcncl lft2rgt dep cls ot = (is_global_exists "core.JMeq.type" hdcncl && jmeq_same_dom env sigma ot)) && not dep then - let c = + let c = match EConstr.kind sigma hdcncl with - | Ind (ind_sp,u) -> - let pr1 = + | Ind (ind_sp,u) -> + let pr1 = lookup_eliminator env ind_sp (elimination_sort_of_clause cls gl) - in + in begin match lft2rgt, cls with | Some true, None | Some false, Some _ -> - let c1 = destConstRef pr1 in + let c1 = destConstRef pr1 in let mp,l = Constant.repr2 (Constant.make1 (Constant.canonical c1)) in - let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in + let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in let c1' = Global.constant_of_delta_kn (KerName.make mp l') in - begin - try - let _ = Global.lookup_constant c1' in - c1' - with Not_found -> + begin + try + let _ = Global.lookup_constant c1' in + c1' + with Not_found -> user_err ~hdr:"Equality.find_elim" (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end - | _ -> destConstRef pr1 + | _ -> destConstRef pr1 end | _ -> (* cannot occur since we checked that we are in presence of Logic.eq or Jmeq just before *) assert false in - pf_constr_of_global (ConstRef c) + pf_constr_of_global (ConstRef c) else let scheme_name = match dep, lft2rgt, inccl with (* Non dependent case *) @@ -946,12 +946,12 @@ let build_coq_I () = pf_constr_of_global (lib_ref "core.True.I") let rec build_discriminator env sigma true_0 false_0 dirn c = function | [] -> let ind = get_type_of env sigma c in - build_selector env sigma dirn c ind true_0 false_0 + build_selector env sigma dirn c ind true_0 (fst false_0) | ((sp,cnum),argnum)::l -> let (cnum_nlams,cnum_env,kont) = descend_then env sigma c cnum in let newc = mkRel(cnum_nlams-argnum) in let subval = build_discriminator cnum_env sigma true_0 false_0 dirn newc l in - kont sigma subval (false_0,mkProp) + kont sigma subval false_0 (* Note: discrimination could be more clever: if some elimination is not allowed because of a large impredicative constructor in the @@ -983,25 +983,22 @@ let gen_absurdity id = absurd_term=False *) -let ind_scheme_of_eq lbeq = +let ind_scheme_of_eq lbeq to_kind = let (mib,mip) = Global.lookup_inductive (destIndRef lbeq.eq) in - let kind = inductive_sort_family mip in + let from_kind = inductive_sort_family mip in (* use ind rather than case by compatibility *) - let kind = - if kind == InProp then Elimschemes.ind_scheme_kind_from_prop - else Elimschemes.ind_scheme_kind_from_type in + let kind = Elimschemes.nondep_elim_scheme from_kind to_kind in let c, eff = find_scheme kind (destIndRef lbeq.eq) in ConstRef c, eff -let discrimination_pf e (t,t1,t2) discriminator lbeq = +let discrimination_pf e (t,t1,t2) discriminator lbeq to_kind = build_coq_I () >>= fun i -> - build_coq_False () >>= fun absurd_term -> - let eq_elim, eff = ind_scheme_of_eq lbeq in + let eq_elim, eff = ind_scheme_of_eq lbeq to_kind in Proofview.tclEFFECTS eff <*> pf_constr_of_global eq_elim >>= fun eq_elim -> Proofview.tclUNIT - (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2]), absurd_term) + (applist (eq_elim, [t;t1;mkNamedLambda (make_annot e Sorts.Relevant) t discriminator;i;t2])) let eq_baseid = Id.of_string "e" @@ -1018,21 +1015,23 @@ let apply_on_clause (f,t) clause = let discr_positions env sigma (lbeq,eqn,(t,t1,t2)) eq_clause cpath dirn = build_coq_True () >>= fun true_0 -> build_coq_False () >>= fun false_0 -> + let false_ty = Retyping.get_type_of env sigma false_0 in + let false_kind = Retyping.get_sort_family_of env sigma false_0 in let e = next_ident_away eq_baseid (vars_of_env env) in let e_env = push_named (Context.Named.Declaration.LocalAssum (make_annot e Sorts.Relevant,t)) env in let discriminator = try Proofview.tclUNIT - (build_discriminator e_env sigma true_0 false_0 dirn (mkVar e) cpath) + (build_discriminator e_env sigma true_0 (false_0,false_ty) dirn (mkVar e) cpath) with UserError _ as ex -> Proofview.tclZERO ex in discriminator >>= fun discriminator -> - discrimination_pf e (t,t1,t2) discriminator lbeq >>= fun (pf, absurd_term) -> - let pf_ty = mkArrow eqn Sorts.Relevant absurd_term in + discrimination_pf e (t,t1,t2) discriminator lbeq false_kind >>= fun pf -> + let pf_ty = mkArrow eqn Sorts.Relevant false_0 in let absurd_clause = apply_on_clause (pf,pf_ty) eq_clause in let pf = Clenvtac.clenv_value_cast_meta absurd_clause in - tclTHENS (assert_after Anonymous absurd_term) + tclTHENS (assert_after Anonymous false_0) [onLastHypId gen_absurdity; (Proofview.V82.tactic (Refiner.refiner ~check:true EConstr.Unsafe.(to_constr pf)))] let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause = diff --git a/tactics/hints.ml b/tactics/hints.ml index cc56c1c425..6fcb37d87c 100644 --- a/tactics/hints.ml +++ b/tactics/hints.ml @@ -1518,7 +1518,7 @@ let pr_hint_term env sigma cl = (* print all hints that apply to the concl of the current goal *) let pr_applicable_hint pf = let env = Global.env () in - let pts = Proof_global.give_me_the_proof pf in + let pts = Proof_global.get_proof pf in let Proof.{goals;sigma} = Proof.data pts in match goals with | [] -> CErrors.user_err Pp.(str "No focused goal.") diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index b9485b8823..539fe31416 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -31,9 +31,9 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects type 'a scheme_kind = string @@ -124,7 +124,7 @@ let define internal role id c poly univs = let entry = { const_entry_body = Future.from_val ((c,Univ.ContextSet.empty), - Safe_typing.empty_private_constants); + Evd.empty_side_effects); const_entry_secctx = None; const_entry_type = None; const_entry_universes = univs; @@ -145,10 +145,10 @@ let define_individual_scheme_base kind suff f mode idopt (mind,i as ind) = let id = match idopt with | Some id -> id | None -> add_suffix mib.mind_packets.(i).mind_typename suff in - let role = Entries.Schema (ind, kind) in + let role = Evd.Schema (ind, kind) in let const, neff = define mode role id c (Declareops.inductive_is_polymorphic mib) ctx in declare_scheme kind [|ind,const|]; - const, Safe_typing.concat_private neff eff + const, Evd.concat_side_effects neff eff let define_individual_scheme kind mode names (mind,i as ind) = match Hashtbl.find scheme_object_table kind with @@ -163,9 +163,9 @@ let define_mutual_scheme_base kind suff f mode names mind = try Int.List.assoc i names with Not_found -> add_suffix mib.mind_packets.(i).mind_typename suff) in let fold i effs id cl = - let role = Entries.Schema ((mind, i), kind)in + let role = Evd.Schema ((mind, i), kind)in let cst, neff = define mode role id cl (Declareops.inductive_is_polymorphic mib) ctx in - (Safe_typing.concat_private neff effs, cst) + (Evd.concat_side_effects neff effs, cst) in let (eff, consts) = Array.fold_left2_map_i fold eff ids cl in let schemes = Array.mapi (fun i cst -> ((mind,i),cst)) consts in @@ -180,7 +180,7 @@ let define_mutual_scheme kind mode names mind = let find_scheme_on_env_too kind ind = let s = String.Map.find kind (Indmap.find ind !scheme_map) in - s, Safe_typing.empty_private_constants + s, Evd.empty_side_effects let find_scheme ?(mode=InternalTacticRequest) kind (mind,i as ind) = try find_scheme_on_env_too kind ind diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index 0eb4e47aeb..460b1f1b07 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -22,9 +22,9 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Evd.side_effects type individual_scheme_object_function = - internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> inductive -> constr Evd.in_evar_universe_context * Evd.side_effects (** Main functions to register a scheme builder *) @@ -39,13 +39,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> Constant.t * Safe_typing.private_constants + Id.t option -> inductive -> Constant.t * Evd.side_effects val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants + (int * Id.t) list -> MutInd.t -> Constant.t array * Evd.side_effects (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Evd.side_effects val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index 59fd8b37d6..81700986ea 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -43,12 +43,8 @@ let tclTHENS = Refiner.tclTHENS let tclTHENSV = Refiner.tclTHENSV let tclTHENSFIRSTn = Refiner.tclTHENSFIRSTn let tclTHENSLASTn = Refiner.tclTHENSLASTn -let tclTHENFIRSTn = Refiner.tclTHENFIRSTn -let tclTHENLASTn = Refiner.tclTHENLASTn let tclREPEAT = Refiner.tclREPEAT -let tclREPEAT_MAIN = Refiner.tclREPEAT_MAIN let tclFIRST = Refiner.tclFIRST -let tclSOLVE = Refiner.tclSOLVE let tclTRY = Refiner.tclTRY let tclCOMPLETE = Refiner.tclCOMPLETE let tclAT_LEAST_ONCE = Refiner.tclAT_LEAST_ONCE @@ -58,10 +54,6 @@ let tclDO = Refiner.tclDO let tclPROGRESS = Refiner.tclPROGRESS let tclSHOWHYPS = Refiner.tclSHOWHYPS let tclTHENTRY = Refiner.tclTHENTRY -let tclIFTHENELSE = Refiner.tclIFTHENELSE -let tclIFTHENSELSE = Refiner.tclIFTHENSELSE -let tclIFTHENSVELSE = Refiner.tclIFTHENSVELSE -let tclIFTHENTRYELSEMUST = Refiner.tclIFTHENTRYELSEMUST (************************************************************************) (* Tacticals applying on hypotheses *) diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 201b7801c3..a9ccda527f 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -31,13 +31,9 @@ val tclTHENLAST : tactic -> tactic -> tactic val tclTHENS : tactic -> tactic list -> tactic val tclTHENSV : tactic -> tactic array -> tactic val tclTHENSLASTn : tactic -> tactic -> tactic array -> tactic -val tclTHENLASTn : tactic -> tactic array -> tactic val tclTHENSFIRSTn : tactic -> tactic array -> tactic -> tactic -val tclTHENFIRSTn : tactic -> tactic array -> tactic val tclREPEAT : tactic -> tactic -val tclREPEAT_MAIN : tactic -> tactic val tclFIRST : tactic list -> tactic -val tclSOLVE : tactic list -> tactic val tclTRY : tactic -> tactic val tclCOMPLETE : tactic -> tactic val tclAT_LEAST_ONCE : tactic -> tactic @@ -49,11 +45,6 @@ val tclSHOWHYPS : tactic -> tactic val tclTHENTRY : tactic -> tactic -> tactic val tclMAP : ('a -> tactic) -> 'a list -> tactic -val tclIFTHENELSE : tactic -> tactic -> tactic -> tactic -val tclIFTHENSELSE : tactic -> tactic list -> tactic -> tactic -val tclIFTHENSVELSE : tactic -> tactic array -> tactic -> tactic -val tclIFTHENTRYELSEMUST : tactic -> tactic -> tactic - (** {6 Tacticals applying to hypotheses } *) val onNthHypId : int -> (Id.t -> tactic) -> tactic |