Add possibility to match on defined hypotheses, using brackets to

disambiguate syntax:
[ H := [ ?x ] : context C [ foo ] |- _ ] is ok, as well as [ H := ?x :
nat |- _ ] or [H := foo |- _ ], but [ H := ?x : context C [ foo ] ] will
not parse.
Add applicative contexts in tactics match, to be able to match arbitrary partial
applications, e.g.: match f 0 1 2 with appcontext C [ f ?x ] => ... end
will bind C to [ ∙ 1 2 ] and x to 0.
Minor improvements in coqdoc.


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

2 files changed, 36 insertions, 8 deletions

diff --git a/pretyping/matching.ml b/pretyping/matching.ml
index ada3b912bf..5162113506 100644
--- a/pretyping/matching.ml
+++ b/pretyping/matching.ml
@@ -202,7 +202,7 @@ let authorized_occ nocc mres =
 let special_meta = (-1)
 
 (* Tries to match a subterm of [c] with [pat] *)
-let rec sub_match nocc pat c =
+let rec sub_match ?(partial_app=false) nocc pat c =
   match kind_of_term c with
   | Cast (c1,k,c2) ->
     (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
@@ -237,13 +237,31 @@ let rec sub_match nocc pat c =
       let (lm,lc) = try_sub_match (nocc - 1) pat [c1;t2;c2] in
       (lm,mkLetIn (x,List.hd lc,List.nth lc 1,List.nth lc 2)))
   | App (c1,lc) ->
-    (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
-    | PatternMatchingFailure ->
-      let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
-      (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
-    | NextOccurrence nocc ->
-      let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
-      (lm,mkApp (List.hd le, Array.of_list (List.tl le))))
+      let rec aux nocc app args =
+	match args with
+	| [] -> 
+	    let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
+	      (lm,mkApp (List.hd le, Array.of_list (List.tl le)))
+	| arg :: args ->
+	    let app = mkApp (app, [|arg|]) in
+	      try let (lm,ce) = sub_match nocc pat app in
+		    (lm,mkApp (ce, Array.of_list args))
+	      with NextOccurrence nocc ->
+		aux nocc app args
+      in
+	(try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
+	| PatternMatchingFailure ->
+	    if partial_app then
+	      aux nocc c1 (Array.to_list lc)
+	    else
+	      let (lm,le) = try_sub_match nocc pat (c1::(Array.to_list lc)) in
+		(lm,mkApp (List.hd le, Array.of_list (List.tl le)))
+	| NextOccurrence nocc ->
+	    if partial_app then
+	      aux nocc c1 (Array.to_list lc)
+	    else
+	      let (lm,le) = try_sub_match (nocc - 1) pat (c1::(Array.to_list lc)) in
+		(lm,mkApp (List.hd le, Array.of_list (List.tl le))))
   | Case (ci,hd,c1,lc) ->
     (try authorized_occ nocc ((matches pat c), mkMeta special_meta) with
     | PatternMatchingFailure ->
@@ -274,6 +292,10 @@ let match_subterm nocc pat c =
   try sub_match nocc pat c
   with NextOccurrence _ -> raise PatternMatchingFailure
 
+let match_appsubterm nocc pat c =
+  try sub_match ~partial_app:true nocc pat c
+  with NextOccurrence _ -> raise PatternMatchingFailure
+
 let is_matching pat n =
   try let _ = matches pat n in true
   with PatternMatchingFailure -> false
diff --git a/pretyping/matching.mli b/pretyping/matching.mli
index b4f6c32451..42f9eab122 100644
--- a/pretyping/matching.mli
+++ b/pretyping/matching.mli
@@ -44,6 +44,12 @@ val matches_conv :env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
    It raises PatternMatchingFailure if no such matching exists *)
 val match_subterm : int -> constr_pattern -> constr -> patvar_map * constr
 
+(* [match_appsubterm n pat c] returns the substitution and the context
+   corresponding to the [n+1]th **closed** subterm of [c] matching [pat], 
+   considering application contexts as well;
+   It raises PatternMatchingFailure if no such matching exists *)
+val match_appsubterm : int -> constr_pattern -> constr -> patvar_map * constr
+
 (* [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
    up to conversion for constants in patterns *)