From 8d5a49accd4052f4594785f8c885dc8c5ea062c8 Mon Sep 17 00:00:00 2001 From: msozeau Date: Tue, 20 Mar 2007 13:48:10 +0000 Subject: Some tactic fixes in Subtac, fix obvious bug in admit_obligations but still a bit broken git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9722 85f007b7-540e-0410-9357-904b9bb8a0f7 --- contrib/subtac/SubtacTactics.v | 22 ++++++++++++++++++++-- contrib/subtac/Utils.v | 4 ++-- contrib/subtac/subtac_obligations.ml | 7 ++++--- 3 files changed, 26 insertions(+), 7 deletions(-) (limited to 'contrib/subtac') diff --git a/contrib/subtac/SubtacTactics.v b/contrib/subtac/SubtacTactics.v index e1c48769c..eac46751e 100644 --- a/contrib/subtac/SubtacTactics.v +++ b/contrib/subtac/SubtacTactics.v @@ -24,19 +24,37 @@ Ltac induction_with_subterms c c' H := Ltac destruct_one_pair := match goal with - | [H : (ex2 _) |- _] => destruct H | [H : (_ /\ _) |- _] => destruct H | [H : prod _ _ |- _] => destruct H end. +Ltac destruct_pairs := repeat (destruct_one_pair). + Ltac destruct_one_ex := let tac H := let ph := fresh "H" in destruct H as [H ph] in match goal with | [H : (ex _) |- _] => tac H | [H : (sig ?P) |- _ ] => tac H + | [H : (ex2 _) |- _] => tac H end. -Ltac destruct_exists := repeat (destruct_one_pair || destruct_one_ex). +Ltac destruct_exists := repeat (destruct_one_ex). + +Ltac destruct_conjs := repeat (destruct_one_pair || destruct_one_ex). + +Ltac on_last_hyp tac := + match goal with + [ H : _ |- _ ] => tac H + end. + +Tactic Notation "on_last_hyp" tactic(t) := on_last_hyp t. + +Ltac revert_last := + match goal with + [ H : _ |- _ ] => revert H + end. + +Ltac reverse := repeat revert_last. Ltac on_call f tac := match goal with diff --git a/contrib/subtac/Utils.v b/contrib/subtac/Utils.v index bf4876a03..67bd70baf 100644 --- a/contrib/subtac/Utils.v +++ b/contrib/subtac/Utils.v @@ -10,7 +10,7 @@ Notation "{ ( x , y ) : A | P }" := Notation " ! " := (False_rect _ _). -Notation "` t" := (proj1_sig t) (at level 100) : core_scope. +Notation " ` t " := (proj1_sig t) (at level 10) : core_scope. Notation "( x & ? )" := (@exist _ _ x _) : core_scope. (** Coerces objects before comparing them *) @@ -29,7 +29,7 @@ Require Import Coq.Bool.Sumbool. Notation "'dec'" := (sumbool_of_bool) (at level 0). (** Default simplification tactic. *) -Ltac subtac_simpl := simpl ; intros ; destruct_exists ; simpl in * ; try subst ; +Ltac subtac_simpl := simpl ; intros ; destruct_conjs ; simpl in * ; try subst ; try (solve [ red ; intros ; discriminate ]) ; auto with *. (** Extraction directives *) diff --git a/contrib/subtac/subtac_obligations.ml b/contrib/subtac/subtac_obligations.ml index b15dd97b1..7295fd24d 100644 --- a/contrib/subtac/subtac_obligations.ml +++ b/contrib/subtac/subtac_obligations.ml @@ -373,9 +373,10 @@ let admit_obligations n = Array.mapi (fun i x -> match x.obl_body with None -> - let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in - assumption_message x.obl_name; - { x with obl_body = Some (mkConst kn) } + let x = subst_deps_obl obls x in + let kn = Declare.declare_constant x.obl_name (ParameterEntry x.obl_type, IsAssumption Conjectural) in + assumption_message x.obl_name; + { x with obl_body = Some (mkConst kn) } | Some _ -> x) obls in -- cgit v1.2.3