- Fixed minor bug #1994 in the tactic chapter of the manual [doc]

- Improved warning when found several path to the same file in path
  [mltop.ml4, system.ml]
- Add support for "rewrite" on specific equality to true (i.e. eq_true)
  [Datatypes.v, tactics] 

PS: compilation test made over 11611 to shunt the archive-breaking 11612 and 11614



git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11617 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 4 insertions, 0 deletions

diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 1e8a5b062..45228073a 100644
--- a/theories/Init/Datatypes.v
+++ b/theories/Init/Datatypes.v
@@ -72,6 +72,10 @@ Hint Resolve andb_true_intro: bool v62.
 
 Inductive eq_true : bool -> Prop := is_eq_true : eq_true true.
 
+(** Technical lemma: identify -> rewriting on eq_true with <- rewriting *)
+
+Definition eq_true_ind_r := eq_true_ind.
+
 (** [nat] is the datatype of natural numbers built from [O] and successor [S];
     note that the constructor name is the letter O.
     Numbers in [nat] can be denoted using a decimal notation;