- 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

2 files changed, 21 insertions, 12 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index 091aa0b8b..870db85ee 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -217,36 +217,37 @@ let pmatches c p = snd (matches_core None true c p)
 let special_meta = (-1)
 
 (* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ pat c mk_ctx next =
+let authorized_occ closed pat c mk_ctx next =
   try 
     let sigma = extended_matches pat c in
-    if not (List.for_all (fun (_,c) -> closed0 c) (snd sigma)) then next ()
+    if closed && not (List.for_all (fun (_,c) -> closed0 c) (snd sigma))
+    then next ()
     else sigma, mk_ctx (mkMeta special_meta), next
   with
     PatternMatchingFailure -> next ()
 
 (* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match ?(partial_app=false) pat c =
+let sub_match ?(partial_app=false) ?(closed=true) pat c =
   let rec aux c mk_ctx next =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
-      authorized_occ pat c mk_ctx (fun () ->
+      authorized_occ closed pat c mk_ctx (fun () ->
         let mk_ctx lc = mk_ctx (mkCast (List.hd lc, k,c2)) in
         try_aux [c1] mk_ctx next)
   | Lambda (x,c1,c2) ->
-      authorized_occ pat c mk_ctx (fun () ->
+      authorized_occ closed pat c mk_ctx (fun () ->
         let mk_ctx lc = mk_ctx (mkLambda (x,List.hd lc,List.nth lc 1)) in
         try_aux [c1;c2] mk_ctx next)
   | Prod (x,c1,c2) ->
-      authorized_occ pat c mk_ctx (fun () ->
+      authorized_occ closed pat c mk_ctx (fun () ->
         let mk_ctx lc = mk_ctx (mkProd (x,List.hd lc,List.nth lc 1)) in
         try_aux [c1;c2] mk_ctx next)
   | LetIn (x,c1,t,c2) ->
-      authorized_occ pat c mk_ctx (fun () ->
+      authorized_occ closed pat c mk_ctx (fun () ->
         let mk_ctx = function [c1;c2] -> mkLetIn (x,c1,t,c2) | _ -> assert false
         in try_aux [c1;c2] mk_ctx next)
   | App (c1,lc) ->
-      authorized_occ pat c mk_ctx (fun () ->
+      authorized_occ closed pat c mk_ctx (fun () ->
         let topdown = true in
 	if partial_app then
           if topdown then
@@ -274,13 +275,13 @@ let rec sub_match ?(partial_app=false) pat c =
             mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
 	  try_aux (c1::Array.to_list lc) mk_ctx next)
   | Case (ci,hd,c1,lc) ->
-      authorized_occ pat c mk_ctx (fun () ->
+      authorized_occ closed pat c mk_ctx (fun () ->
         let mk_ctx le = 
           mk_ctx (mkCase (ci,hd,List.hd le,Array.of_list (List.tl le))) in
         try_aux (c1::Array.to_list lc) mk_ctx next)
   | Construct _ | Fix _ | Ind _|CoFix _ |Evar _|Const _
   | Rel _|Meta _|Var _|Sort _ ->
-      authorized_occ pat c mk_ctx next
+      authorized_occ closed pat c mk_ctx next
 
   (* Tries [sub_match] for all terms in the list *)
   and try_aux lc mk_ctx next =
@@ -302,8 +303,12 @@ let match_appsubterm pat c = sub_match ~partial_app:true pat c
 
 let match_subterm_gen app pat c = sub_match ~partial_app:app pat c
 
-let is_matching pat n =
-  try let _ = matches pat n in true
+let is_matching pat c =
+  try let _ = matches pat c in true
+  with PatternMatchingFailure -> false
+
+let is_matching_appsubterm ?(closed=true) pat c =
+  try let _ = sub_match ~partial_app:true ~closed pat c in true
   with PatternMatchingFailure -> false
 
 let matches_conv env sigma c p =
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index 574a4bbd2..4b3bc6c05 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -69,6 +69,10 @@ val match_appsubterm : constr_pattern -> constr -> subterm_matching_result
 val match_subterm_gen : bool (* true = with app context *) -> 
    constr_pattern -> constr -> subterm_matching_result
 
+(* [is_matching_appsubterm pat c] tells if a subterm of [c] matches
+   against [pat] taking partial subterms into consideration *)
+val is_matching_appsubterm : ?closed:bool -> constr_pattern -> constr -> bool
+
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
    up to conversion for constants in patterns *)
 val is_matching_conv :