diff options
| -rw-r--r-- | contrib/subtac/SubtacTactics.v | 13 | ||||
| -rw-r--r-- | contrib/subtac/Utils.v | 7 | ||||
| -rw-r--r-- | contrib/subtac/g_subtac.ml4 | 10 | ||||
| -rw-r--r-- | contrib/subtac/subtac_cases.ml | 4 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.ml | 10 | ||||
| -rw-r--r-- | contrib/subtac/subtac_obligations.mli | 5 |
6 files changed, 43 insertions, 6 deletions
diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v index d1e3caf7d..d38902c96 100644 --- a/contrib/subtac/SubtacTactics.v +++ b/contrib/subtac/SubtacTactics.v @@ -40,6 +40,19 @@ Ltac destruct_one_ex := Ltac destruct_exists := repeat (destruct_one_ex). +Tactic Notation "destruct" "exist" ident(t) ident(Ht) := destruct t as [t Ht]. + +Tactic Notation "destruct" "or" ident(H) := destruct H as [H|H]. + +Tactic Notation "contradiction" "by" constr(t) := + let H := fresh in assert t as H by auto with * ; contradiction. + +Ltac discriminates := + match goal with + | [ H : ?x <> ?x |- _ ] => elim H ; reflexivity + | _ => discriminate + end. + Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). Ltac on_last_hyp tac := diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index 137ac8c98..a83a321de 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -25,9 +25,14 @@ Notation "'forall' { x : A | P } , Q" := (forall x:{x:A|P}, Q) (at level 200, x ident, right associativity). -Require Import Coq.Bool.Sumbool. +Require Import Coq.Bool.Sumbool. +(** Construct a dependent disjunction from a boolean. *) Notation "'dec'" := (sumbool_of_bool) (at level 0). +(** The notations [in_right] and [in_left] construct objects of a dependent disjunction. *) +Notation in_right := (@right _ _ _). +Notation in_left := (@left _ _ _). + (** Default simplification tactic. *) Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; try (solve [ red ; intros ; discriminate ]) ; auto with *. diff --git a/contrib/subtac/g_subtac.ml4 b/contrib/subtac/g_subtac.ml4 index 9e9a76707..05334ad76 100644 --- a/contrib/subtac/g_subtac.ml4 +++ b/contrib/subtac/g_subtac.ml4 @@ -111,6 +111,16 @@ VERNAC COMMAND EXTEND Subtac_Solve_Obligations [ Subtac_obligations.try_solve_obligations None (Tacinterp.interp t) ] | [ "Solve" "Obligations" ] -> [ Subtac_obligations.try_solve_obligations None (Subtac_obligations.default_tactic ()) ] + END + +VERNAC COMMAND EXTEND Subtac_Solve_All_Obligations +| [ "Solve" "All" "Obligations" "using" tactic(t) ] -> + [ Subtac_obligations.solve_all_obligations (Tacinterp.interp t) ] +| [ "Solve" "All" "Obligations" ] -> + [ Subtac_obligations.solve_all_obligations (Subtac_obligations.default_tactic ()) ] + END + +VERNAC COMMAND EXTEND Subtac_Admit_Obligations | [ "Admit" "Obligations" "of" ident(name) ] -> [ Subtac_obligations.admit_obligations (Some name) ] | [ "Admit" "Obligations" ] -> [ Subtac_obligations.admit_obligations None ] END diff --git a/contrib/subtac/subtac_cases.ml b/contrib/subtac/subtac_cases.ml index cbfff99e8..7f71bfa72 100644 --- a/contrib/subtac/subtac_cases.ml +++ b/contrib/subtac/subtac_cases.ml @@ -1755,8 +1755,8 @@ let build_ineqs prevpatterns pats liftsign = succ n, (* nth pattern *) mkApp (Lazy.force eq_ind, [| lift (lens + liftsign) ppat_ty ; - ppat_c ; - (*liftn liftsign lens ppat_c ; *) +(* ppat_c ; *) + liftn liftsign (succ lens) ppat_c ; lift len' curpat_c |]) :: List.map (fun t -> diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index d19e86786..3c8fd1d45 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -352,8 +352,7 @@ and solve_obligation_by_tac prg obls i tac = else false with _ -> false) -and solve_obligations n tac = - let prg = get_prog n in +and solve_prg_obligations prg tac = let obls, rem = prg.prg_obligations in let rem = ref rem in let obls' = Array.copy obls in @@ -364,6 +363,13 @@ and solve_obligations n tac = obls' in update_obls prg obls' !rem + +and solve_obligations n tac = + let prg = get_prog n in + solve_prg_obligations prg tac + +and solve_all_obligations tac = + ProgMap.iter (fun k v -> ignore(solve_prg_obligations v tac)) !from_prg and try_solve_obligations n tac = ignore (solve_obligations n tac) diff --git a/contrib/subtac/subtac_obligations.mli b/contrib/subtac/subtac_obligations.mli index 0ad9e730d..8a6455136 100644 --- a/contrib/subtac/subtac_obligations.mli +++ b/contrib/subtac/subtac_obligations.mli @@ -17,7 +17,10 @@ val subtac_obligation : int * Names.identifier option * Topconstr.constr_expr op val next_obligation : Names.identifier option -> unit val solve_obligations : Names.identifier option -> Proof_type.tactic -> int - (* Number of remaining obligations to be solved for this program *) +(* Number of remaining obligations to be solved for this program *) + +val solve_all_obligations : Proof_type.tactic -> unit + val try_solve_obligations : Names.identifier option -> Proof_type.tactic -> unit val show_obligations : Names.identifier option -> unit |