- Added support for subterm matching in SearchAbout.

- Backtrack on precise unfolding of "iff" in "tauto": it has effects on
  the naming of hypotheses (especially when doing "case H" with H of
  type "{x|P<->Q}" since not unfolding will eventually introduce a name
  "i" while unfolding will eventually introduce a name "a" (deep sigh).
- Miscellaneous (error when a plugin is missing, doc hnf, standardization
  of names manipulating type constr_pattern, ...).



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

8 files changed, 26 insertions, 34 deletions

diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 48a7a7a5a..bcb2f7a57 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -615,11 +615,12 @@ GEXTEND Gram
       | IDENT "SearchAbout"; 
 	  sl = [ "[";
 	         l = LIST1 [ 
-		   b = positive_search_mark; r = global -> b,SearchRef r
-		 | b = positive_search_mark; s = ne_string; sc = OPT scope
-		   -> b,SearchString (s,sc)
+		   b = positive_search_mark; s = ne_string; sc = OPT scope
+		   -> b, SearchString (s,sc)
+		 | b = positive_search_mark; p = constr_pattern
+		   -> b, SearchSubPattern p
 		 ]; "]" -> l
-   	       | qid = global -> [true,SearchRef qid]
+   	       | p = constr_pattern -> [true,SearchSubPattern p]
    	       | s = ne_string; sc = OPT scope -> [true,SearchString (s,sc)] ];
 	  l = in_or_out_modules -> 
 	  VernacSearch (SearchAbout sl, l)
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index f5fe151ed..e16641a83 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -666,15 +666,15 @@ let rec strip_context n iscast t =
 type term_pr = {
   pr_constr_expr   : constr_expr -> std_ppcmds;
   pr_lconstr_expr  : constr_expr -> std_ppcmds;
-  pr_pattern_expr  : Tacexpr.pattern_expr -> std_ppcmds;
-  pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
 }
 
 let default_term_pr = {
   pr_constr_expr   = pr lsimple;
   pr_lconstr_expr  = pr ltop;
-  pr_pattern_expr  = pr lsimple;
-  pr_lpattern_expr = pr ltop
+  pr_constr_pattern_expr  = pr lsimple;
+  pr_lconstr_pattern_expr = pr ltop
 }
 
 let term_pr = ref default_term_pr
@@ -683,8 +683,8 @@ let set_term_pr = (:=) term_pr
 
 let pr_constr_expr c   = !term_pr.pr_constr_expr   c
 let pr_lconstr_expr c  = !term_pr.pr_lconstr_expr  c
-let pr_pattern_expr c  = !term_pr.pr_pattern_expr  c
-let pr_lpattern_expr c = !term_pr.pr_lpattern_expr c
+let pr_constr_pattern_expr c  = !term_pr.pr_constr_pattern_expr  c
+let pr_lconstr_pattern_expr c = !term_pr.pr_lconstr_pattern_expr c
 
 let pr_cases_pattern_expr = pr_patt ltop
 
diff --git a/parsing/ppconstr.mli b/parsing/ppconstr.mli
index b9bf933eb..d7fdd1ed9 100644
--- a/parsing/ppconstr.mli
+++ b/parsing/ppconstr.mli
@@ -66,8 +66,8 @@ val pr_may_eval :
 val pr_rawsort : rawsort -> std_ppcmds
 
 val pr_binders : local_binder list -> std_ppcmds
-val pr_pattern_expr : Tacexpr.pattern_expr -> std_ppcmds
-val pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds
+val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
 val pr_constr_expr : constr_expr -> std_ppcmds
 val pr_lconstr_expr : constr_expr -> std_ppcmds
 val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
@@ -75,8 +75,8 @@ val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds
 type term_pr = {
   pr_constr_expr   : constr_expr -> std_ppcmds;
   pr_lconstr_expr  : constr_expr -> std_ppcmds;
-  pr_pattern_expr  : Tacexpr.pattern_expr -> std_ppcmds;
-  pr_lpattern_expr : Tacexpr.pattern_expr -> std_ppcmds
+  pr_constr_pattern_expr  : constr_pattern_expr -> std_ppcmds;
+  pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds
 }
 
 val set_term_pr : term_pr -> unit
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index 7cb93d108..2f102488f 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -1024,7 +1024,7 @@ let rec raw_printers =
     (pr_raw_tactic_level, 
      drop_env pr_constr_expr,
      drop_env pr_lconstr_expr,
-     pr_lpattern_expr,
+     pr_lconstr_pattern_expr,
      drop_env (pr_or_by_notation pr_reference),
      drop_env (pr_or_by_notation pr_reference),
      pr_reference,
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index a3eed62b7..df4eee8aa 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -136,7 +136,7 @@ let pr_in_out_modules = function
 let pr_search_about (b,c) = 
   (if b then str "-" else mt()) ++
   match c with
-  | SearchRef r -> pr_reference r
+  | SearchSubPattern p -> pr_constr_pattern_expr p
   | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc
 
 let pr_search a b pr_p = match a with
@@ -819,7 +819,7 @@ let rec pr_vernac = function
   | VernacCreateHintDb (local,dbname,b) ->
       hov 1 (str "Create " ++ pr_locality local ++ str "HintDb " ++ str dbname ++ (if b then str" discriminated" else mt ()))
   | VernacHints (local,dbnames,h) ->
-      pr_hints local dbnames h pr_constr pr_pattern_expr
+      pr_hints local dbnames h pr_constr pr_constr_pattern_expr
   | VernacSyntacticDefinition (id,(ids,c),local,onlyparsing) ->
       hov 2
         (str"Notation " ++ pr_locality local ++ pr_lident id ++ 
@@ -912,7 +912,7 @@ let rec pr_vernac = function
          term *)
 	| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
       in pr_printable p
-  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_pattern_expr
+  | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc -> 
       let pr_locate =function
 	| LocateTerm qid ->  pr_reference qid
diff --git a/parsing/printer.ml b/parsing/printer.ml
index bfb571b23..e2150fcbf 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -89,14 +89,14 @@ let pr_cases_pattern t =
   pr_cases_pattern_expr (extern_cases_pattern Idset.empty t)
 
 let pr_lconstr_pattern_env env c =
-  pr_lconstr_expr (extern_constr_pattern (names_of_rel_context env) c)
+  pr_lconstr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
 let pr_constr_pattern_env env c =
-  pr_constr_expr (extern_constr_pattern (names_of_rel_context env) c)
+  pr_constr_pattern_expr (extern_constr_pattern (names_of_rel_context env) c)
 
 let pr_lconstr_pattern t =
-  pr_lconstr_expr (extern_constr_pattern empty_names_context t)
+  pr_lconstr_pattern_expr (extern_constr_pattern empty_names_context t)
 let pr_constr_pattern t =
-  pr_constr_expr (extern_constr_pattern empty_names_context t)
+  pr_constr_pattern_expr (extern_constr_pattern empty_names_context t)
 
 let pr_sort s = pr_rawsort (extern_sort s)
 
diff --git a/parsing/search.ml b/parsing/search.ml
index 49682ee48..94270ee13 100644
--- a/parsing/search.ml
+++ b/parsing/search.ml
@@ -165,15 +165,6 @@ let raw_search_rewrite extra_filter display_function pattern =
         (pattern_filter (mk_rewrite_pattern2 gref_eq pattern) s a c)) 
        && extra_filter s a c)
     display_function gref_eq
-(*
-  ;
-  filtered_search
-    (fun s a c ->
-       ((pattern_filter (mk_rewrite_pattern1 gref_eqT pattern) s a c) ||
-        (pattern_filter (mk_rewrite_pattern2 gref_eqT pattern) s a c)) 
-       && extra_filter s a c)
-    display_function gref_eqT
-*)
 
 let text_pattern_search extra_filter =
   raw_pattern_search extra_filter plain_display
@@ -204,11 +195,11 @@ let gen_filtered_search filter_function display_function =
 let name_of_reference ref = string_of_id (id_of_global ref)
 
 type glob_search_about_item =
-  | GlobSearchRef of global_reference
+  | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
 let search_about_item (itemref,typ) = function
-  | GlobSearchRef ref -> Termops.occur_term (constr_of_global ref) typ
+  | GlobSearchSubPattern pat -> is_matching_appsubterm ~closed:false pat typ
   | GlobSearchString s -> string_string_contains (name_of_reference itemref) s
 
 let raw_search_about filter_modules display_function l =
diff --git a/parsing/search.mli b/parsing/search.mli
index 356c5b469..fc2ea925f 100644
--- a/parsing/search.mli
+++ b/parsing/search.mli
@@ -19,7 +19,7 @@ open Nametab
 (*s Search facilities. *)
 
 type glob_search_about_item =
-  | GlobSearchRef of global_reference
+  | GlobSearchSubPattern of constr_pattern
   | GlobSearchString of string
 
 val search_by_head : global_reference -> dir_path list * bool -> unit