From f8e2c78e8bfd8679a77e3cf676bde58c4efffd45 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 29 Jun 2009 19:15:14 +0000
Subject: Miscellaneous practical commits: - theories: made a hint database
 with the constructor of eq_true - coqide: binding F5 to About dans coqide +
 made coqide aware of   string interpretation inside comments - lexer: added
 warning when ending comments inside a strings itself in a comment - xlate:
 completed patten-matching on IntroForthComing

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12217 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 theories/Init/Datatypes.v | 2 ++
 theories/Init/Tactics.v   | 2 +-
 2 files changed, 3 insertions(+), 1 deletion(-)

(limited to 'theories')

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 2194b93a3f..84af2fe852 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -74,6 +74,8 @@ Hint Resolve andb_true_intro: bool.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
+Hint Constructors eq_true : eq_true.
+
 (** Additional rewriting lemmas about [eq_true] *)
 
 Lemma eq_true_ind_r :
diff --git a/theories/Init/Tactics.v b/theories/Init/Tactics.v
index a59eba6f46..52b5012a9b 100644
--- a/theories/Init/Tactics.v
+++ b/theories/Init/Tactics.v
@@ -167,7 +167,7 @@ Ltac easy :=
     solve [reflexivity | symmetry; trivial] ||
     contradiction ||
     (split; do_atom)
-  with do_ccl := trivial; repeat do_intro; do_atom in
+  with do_ccl := trivial with eq_true; repeat do_intro; do_atom in
   (use_hyps; do_ccl) || fail "Cannot solve this goal".
 
 Tactic Notation "now" tactic(t) := t; easy.
-- 
cgit v1.2.3