diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-08 13:39:01 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-10-08 13:39:01 +0000 |
| commit | 93b74b4be215bd08ca7a123505177d6ec8ac7b4c (patch) | |
| tree | cc5b80a8ba038a7c531afae977234f2afdc70699 /theories/Program/Equality.v | |
| parent | bdec9fddcdaa13800e04e718ffa52f87bddc52d9 (diff) | |
Init/Tactics.v: tactic with nicer name 'exfalso' for 'elimtype False'
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12380 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'theories/Program/Equality.v')
| -rw-r--r-- | theories/Program/Equality.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index ca65f3bbe..0c77a1325 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -374,7 +374,7 @@ Ltac simplify_one_dep_elim_term c := | @eq ?A ?t ?u -> ?P => apply (noConfusion (I:=A) P) | ?f ?x = ?g ?y -> _ => let H := fresh in progress (intros H ; injection H ; clear H) | ?t = ?u -> _ => let hyp := fresh in - intros hyp ; elimtype False ; discriminate + intros hyp ; exfalso ; discriminate | ?x = ?y -> _ => let hyp := fresh in intros hyp ; (try (clear hyp ; (* If non dependent, don't clear it! *) fail 1)) ; case hyp ; clear hyp @@ -447,7 +447,7 @@ Ltac try_intros m := (** To solve a goal by inversion on a particular target. *) Ltac solve_empty target := - do_nat target intro ; elimtype False ; destruct_last ; simplify_dep_elim. + do_nat target intro ; exfalso ; destruct_last ; simplify_dep_elim. Ltac simplify_method tac := repeat (tac || simplify_one_dep_elim) ; reverse_local. |