summaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
authorGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
committerGravatar Stephane Glondu <steph@glondu.net>2012-06-04 12:07:52 +0200
commit61dc740ed1c3780cccaec00d059a28f0d31d0052 (patch)
treed88d05baf35b9b09a034233300f35a694f9fa6c2 /theories/Program
parent97fefe1fcca363a1317e066e7f4b99b9c1e9987b (diff)
Imported Upstream version 8.4~gamma0+really8.4beta2upstream/8.4_gamma0+really8.4beta2
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Equality.v26
1 files changed, 18 insertions, 8 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v
index 06ff7cd1..d408845e 100644
--- a/theories/Program/Equality.v
+++ b/theories/Program/Equality.v
@@ -28,7 +28,7 @@ Hint Extern 10 => is_ground_goal ; progress exfalso : exfalso.
Definition block {A : Type} (a : A) := a.
Ltac block_goal := match goal with [ |- ?T ] => change (block T) end.
-Ltac unblock_goal := cbv beta delta [block].
+Ltac unblock_goal := unfold block in *.
(** Notation for heterogenous equality. *)
@@ -214,7 +214,8 @@ Ltac simplify_eqs :=
Ltac simplify_IH_hyps := repeat
match goal with
- | [ hyp : _ |- _ ] => specialize_eqs hyp
+ | [ hyp : context [ block _ ] |- _ ] =>
+ specialize_eqs hyp
end.
(** We split substitution tactics in the two directions depending on which
@@ -377,14 +378,23 @@ Ltac is_introduced H :=
end.
Tactic Notation "intro_block" hyp(H) :=
- (is_introduced H ; block_goal ; revert_until H) ||
+ (is_introduced H ; block_goal ; revert_until H ; block_goal) ||
(let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
Tactic Notation "intro_block_id" ident(H) :=
- (is_introduced H ; block_goal ; revert_until H) ||
+ (is_introduced H ; block_goal ; revert_until H; block_goal) ||
(let H' := fresh H in intros until H' ; block_goal) || (intros ; block_goal).
-Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
+Ltac unblock_dep_elim :=
+ match goal with
+ | |- block ?T =>
+ match T with context [ block _ ] =>
+ change T ; intros ; unblock_goal
+ end
+ | _ => unblock_goal
+ end.
+
+Ltac simpl_dep_elim := simplify_dep_elim ; simplify_IH_hyps ; unblock_dep_elim.
Ltac do_intros H :=
(try intros until H) ; (intro_block_id H || intro_block H).
@@ -395,7 +405,7 @@ Ltac do_depelim tac H := do_depelim_nosimpl tac H ; simpl_dep_elim.
Ltac do_depind tac H :=
(try intros until H) ; intro_block H ;
- generalize_eqs_vars H ; tac H ; simplify_dep_elim ; simplify_IH_hyps ; unblock_goal.
+ generalize_eqs_vars H ; tac H ; simpl_dep_elim.
(** To dependent elimination on some hyp. *)
@@ -412,8 +422,8 @@ Ltac depind id := do_depind ltac:(fun hyp => do_ind hyp) id.
(** A variant where generalized variables should be given by the user. *)
Ltac do_depelim' rev tac H :=
- (try intros until H) ; block_goal ; rev H ; generalize_eqs H ; tac H ; simplify_dep_elim ;
- simplify_IH_hyps ; unblock_goal.
+ (try intros until H) ; block_goal ; rev H ;
+ (try revert_until H ; block_goal) ; generalize_eqs H ; tac H ; simpl_dep_elim.
(** Calls [destruct] on the generalized hypothesis, results should be similar to inversion.
By default, we don't try to generalize the hyp by its variable indices. *)