diff options
Diffstat (limited to 'tactics/hiddentac.ml')
| -rw-r--r-- | tactics/hiddentac.ml | 142 |
1 files changed, 0 insertions, 142 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml deleted file mode 100644 index 8bfebc03..00000000 --- a/tactics/hiddentac.ml +++ /dev/null @@ -1,142 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Term -open Proof_type -open Tacmach - -open Glob_term -open Refiner -open Genarg -open Tacexpr -open Tactics -open Util - -(* Basic tactics *) -let h_intro_move x y = - abstract_tactic (TacIntroMove (x, y)) (intro_move x y) -let h_intro x = h_intro_move (Some x) no_move -let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) -let h_assumption = abstract_tactic TacAssumption assumption -let h_exact c = abstract_tactic (TacExact c) (exact_check c) -let h_exact_no_check c = - abstract_tactic (TacExactNoCheck c) (exact_no_check c) -let h_vm_cast_no_check c = - abstract_tactic (TacVmCastNoCheck c) (vm_cast_no_check c) -let h_apply simple ev cb = - abstract_tactic (TacApply (simple,ev,List.map snd cb,None)) - (apply_with_bindings_gen simple ev cb) -let h_apply_in simple ev cb (id,ipat as inhyp) = - abstract_tactic (TacApply (simple,ev,List.map snd cb,Some inhyp)) - (apply_in simple ev id cb ipat) -let h_elim ev cb cbo = - abstract_tactic (TacElim (ev,cb,cbo)) - (elim ev cb cbo) -let h_elim_type c = abstract_tactic (TacElimType c) (elim_type c) -let h_case ev cb = abstract_tactic (TacCase (ev,cb)) (general_case_analysis ev cb) -let h_case_type c = abstract_tactic (TacCaseType c) (case_type c) -let h_fix ido n = abstract_tactic (TacFix (ido,n)) (fix ido n) -let h_mutual_fix b id n l = - abstract_tactic - (TacMutualFix (b,id,n,l)) - (mutual_fix id n l 0) - -let h_cofix ido = abstract_tactic (TacCofix ido) (cofix ido) -let h_mutual_cofix b id l = - abstract_tactic - (TacMutualCofix (b,id,l)) - (mutual_cofix id l 0) - -let h_cut c = abstract_tactic (TacCut c) (cut c) -let h_generalize_gen cl = - abstract_tactic (TacGeneralize cl) - (generalize_gen (List.map (on_fst Redexpr.out_with_occurrences) cl)) -let h_generalize cl = - h_generalize_gen (List.map (fun c -> ((all_occurrences_expr,c),Names.Anonymous)) - cl) -let h_generalize_dep c = - abstract_tactic (TacGeneralizeDep c) (generalize_dep c) -let h_let_tac b na c cl eqpat = - let id = Option.default (dummy_loc,IntroAnonymous) eqpat in - let with_eq = if b then None else Some (true,id) in - abstract_tactic (TacLetTac (na,c,cl,b,eqpat)) - (letin_tac with_eq na c None cl) -let h_let_pat_tac b na c cl eqpat = - let id = Option.default (dummy_loc,IntroAnonymous) eqpat in - let with_eq = if b then None else Some (true,id) in - abstract_tactic (TacLetTac (na,snd c,cl,b,eqpat)) - (letin_pat_tac with_eq na c None cl) - -(* Derived basic tactics *) -let h_simple_induction_destruct isrec h = - abstract_tactic (TacSimpleInductionDestruct (isrec,h)) - (if isrec then (simple_induct h) else (simple_destruct h)) -let h_simple_induction = h_simple_induction_destruct true -let h_simple_destruct = h_simple_induction_destruct false - -let out_indarg = function - | ElimOnConstr (_,c) -> ElimOnConstr c - | ElimOnIdent id -> ElimOnIdent id - | ElimOnAnonHyp n -> ElimOnAnonHyp n - -let h_induction_destruct isrec ev lcl = - let lcl' = on_pi1 (List.map (fun (a,b) ->(out_indarg a,b))) lcl in - abstract_tactic (TacInductionDestruct (isrec,ev,lcl')) - (induction_destruct isrec ev lcl) -let h_new_induction ev c idl e cl = - h_induction_destruct true ev ([c,idl],e,cl) -let h_new_destruct ev c idl e cl = h_induction_destruct false ev ([c,idl],e,cl) - -let h_specialize n d = abstract_tactic (TacSpecialize (n,d)) (specialize n d) -let h_lapply c = abstract_tactic (TacLApply c) (cut_and_apply c) - -(* Context management *) -let h_clear b l = abstract_tactic (TacClear (b,l)) - ((if b then keep else clear) l) -let h_clear_body l = abstract_tactic (TacClearBody l) (clear_body l) -let h_move dep id1 id2 = - abstract_tactic (TacMove (dep,id1,id2)) (move_hyp dep id1 id2) -let h_rename l = - abstract_tactic (TacRename l) (rename_hyp l) -let h_revert l = abstract_tactic (TacRevert l) (revert l) - -(* Constructors *) -let h_left ev l = abstract_tactic (TacLeft (ev,l)) (left_with_bindings ev l) -let h_right ev l = abstract_tactic (TacRight (ev,l)) (right_with_bindings ev l) -let h_split ev l = abstract_tactic (TacSplit (ev,false,l)) (split_with_bindings ev l) -(* Moved to tacinterp because of dependencies in Tacinterp.interp -let h_any_constructor t = - abstract_tactic (TacAnyConstructor t) (any_constructor t) -*) -let h_constructor ev n l = - abstract_tactic (TacConstructor(ev,ArgArg n,l))(constructor_tac ev None n l) -let h_one_constructor n = - abstract_tactic (TacConstructor(false,ArgArg n,NoBindings)) (one_constructor n NoBindings) -let h_simplest_left = h_left false NoBindings -let h_simplest_right = h_right false NoBindings - -(* Conversion *) -let h_reduce r cl = - abstract_tactic (TacReduce (r,cl)) (reduce r cl) -let h_change op c cl = - abstract_tactic (TacChange (op,c,cl)) (change op c cl) - -(* Equivalence relations *) -let h_reflexivity = abstract_tactic TacReflexivity intros_reflexivity -let h_symmetry c = abstract_tactic (TacSymmetry c) (intros_symmetry c) -let h_transitivity c = - abstract_tactic (TacTransitivity c) - (intros_transitivity c) - -let h_simplest_apply c = h_apply false false [dummy_loc,(c,NoBindings)] -let h_simplest_eapply c = h_apply false true [dummy_loc,(c,NoBindings)] -let h_simplest_elim c = h_elim false (c,NoBindings) None -let h_simplest_case c = h_case false (c,NoBindings) - -let h_intro_patterns l = abstract_tactic (TacIntroPattern l) (intro_patterns l) - |