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

6 files changed, 32 insertions, 6 deletions

diff --git a/ide/coqide.ml b/ide/coqide.ml
index 14a0fd037..01aef20fc 100644
--- a/ide/coqide.ml
+++ b/ide/coqide.ml
@@ -2841,6 +2841,14 @@ with _ := Induction for _ Sort _.\n",61,10, Some GdkKeysyms._S);
 								       ())
 					  in
 					  let _ = 
+					    queries_factory#add_item "_About " ~key:GdkKeysyms._F5
+					      ~callback:(fun () -> let term = get_current_word () in
+								     (Command_windows.command_window ())#new_command
+								       ~command:"About"
+								       ~term 
+								       ())
+					  in
+					  let _ = 
 					    queries_factory#add_item "_Locate" 
 					      ~callback:(fun () -> let term = get_current_word () in
 								     (Command_windows.command_window ())#new_command
diff --git a/ide/highlight.mll b/ide/highlight.mll
index b791aa509..4b36414d6 100644
--- a/ide/highlight.mll
+++ b/ide/highlight.mll
@@ -139,9 +139,16 @@ and next_interior_order = parse
 and comment = parse
   | "*)" { !comment_start,lexeme_end lexbuf,"comment" }
   | "(*" { ignore (comment lexbuf); comment lexbuf }
+  | "\"" { string_in_comment lexbuf }
   | _    { comment lexbuf }
   | eof  { raise End_of_file }
 
+and string_in_comment = parse
+  | "\"\"" { string_in_comment lexbuf }
+  | "\"" { comment lexbuf }
+  | _ { string_in_comment lexbuf }
+  | eof  { raise End_of_file }
+
 {
   open Ideutils
 
diff --git a/parsing/lexer.ml4 b/parsing/lexer.ml4
index 7a1421592..008a0f0b5 100644
--- a/parsing/lexer.ml4
+++ b/parsing/lexer.ml4
@@ -248,10 +248,18 @@ let rec number len = parser
 
 let escape len c = store len c
 
-let rec string bp len = parser
+let rec string in_comments bp len = parser
   | [< ''"'; esc=(parser [<''"' >] -> true | [< >] -> false); s >] ->
-      if esc then string bp (store len '"') s else len
-  | [< 'c; s >] -> string bp (store len c) s 
+      if esc then string in_comments bp (store len '"') s else len
+  | [< ''*'; s >] ->
+      (parser
+        | [< '')'; s >] -> 
+	    if in_comments then
+	      warning "Not interpreting \"*)\" as the end of current non-terminated comment because it occurs in a non-terminated string of the comment.";
+	    string in_comments bp (store (store len '*') ')') s 
+        | [< >] ->
+	    string in_comments bp (store len '*') s) s
+  | [< 'c; s >] -> string in_comments bp (store len c) s 
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_string
 
 (* Hook for exporting comment into xml theory files *)
@@ -337,7 +345,7 @@ let rec comment bp = parser bp2
          | [< s >] -> real_push_char '*'; comment bp s >] -> ()
   | [< ''"'; s >] ->
       if Flags.do_beautify() then (push_string"\"";comm_string bp2 s)
-      else ignore (string bp2 0 s);
+      else ignore (string true bp2 0 s);
       comment bp s
   | [< _ = Stream.empty >] ep -> err (bp, ep) Unterminated_comment
   | [< 'z; s >] -> real_push_char z; comment bp s
@@ -446,7 +454,7 @@ let rec next_token = parser bp
   | [< ' ('0'..'9' as c); len = number (store 0 c) >] ep ->
       comment_stop bp;
       (("INT", get_buff len), (bp, ep))
-  | [< ''\"'; len = string bp 0 >] ep ->
+  | [< ''\"'; len = string false bp 0 >] ep ->
       comment_stop bp;
       (("STRING", get_buff len), (bp, ep))
   | [< ' ('(' as c);
diff --git a/plugins/interface/xlate.ml b/plugins/interface/xlate.ml
index d1e2b03ef..1f4038cbb 100644
--- a/plugins/interface/xlate.ml
+++ b/plugins/interface/xlate.ml
@@ -635,6 +635,7 @@ let rec xlate_intro_pattern (loc,pat) = match pat with
   | IntroAnonymous -> xlate_error "TODO: IntroAnonymous"
   | IntroFresh _ -> xlate_error "TODO: IntroFresh"
   | IntroRewrite _ -> xlate_error "TODO: IntroRewrite"
+  | IntroForthcoming _ -> xlate_error "TODO: IntroForthcoming"
 
 let compute_INV_TYPE = function
    FullInversionClear -> CT_inv_clear
diff --git a/theories/Init/Datatypes.v b/theories/Init/Datatypes.v
index 2194b93a3..84af2fe85 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 a59eba6f4..52b5012a9 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.