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

3 files changed, 30 insertions, 10 deletions

diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index cd10e51f1..d9bc8038b 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -165,11 +165,24 @@ GEXTEND Gram
   match_pattern:
     [ [ IDENT "context";  oid = OPT Constr.ident;
           "["; pc = Constr.lconstr_pattern; "]" ->
-        Subterm (oid, pc)
+        Subterm (false,oid, pc)
+      | IDENT "appcontext";  oid = OPT Constr.ident;
+          "["; pc = Constr.lconstr_pattern; "]" ->
+        Subterm (true,oid, pc)
       | pc = Constr.lconstr_pattern -> Term pc ] ]
   ;
   match_hyps:
-    [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp) ] ]
+    [ [ na = name; ":"; mp =  match_pattern -> Hyp (na, mp) 
+      | na = name; ":="; "["; mpv = match_pattern; "]"; ":"; mpt = match_pattern -> Def (na, mpv, mpt) 
+      | na = name; ":="; mpv = match_pattern -> 
+	  let t, ty =
+	    match mpv with 
+	    | Term t -> (match t with
+	      | CCast (loc, t, CastConv (_, ty)) -> Term t, Some (Term ty)
+	      | _ -> mpv, None)
+	    | _ -> mpv, None
+	  in Def (na, t, Option.default (Term (CHole (dummy_loc, None))) ty)
+    ] ]
   ;
   match_context_rule:
     [ [ largs = LIST0 match_hyps SEP ","; "|-"; mp = match_pattern;
diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml
index e59df48aa..3d1eec4fe 100644
--- a/parsing/pptactic.ml
+++ b/parsing/pptactic.ml
@@ -458,12 +458,16 @@ let pr_lazy lz = if lz then str "lazy " else mt ()
 
 let pr_match_pattern pr_pat = function
   | Term a -> pr_pat a
-  | Subterm (None,a) -> str "context [" ++ pr_pat a ++ str "]"
-  | Subterm (Some id,a) ->
-      str "context " ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
-
-let pr_match_hyps pr_pat (Hyp (nal,mp)) =
-  pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Subterm (b,None,a) -> (if b then str"appcontext [" else str "context [") ++ pr_pat a ++ str "]"
+  | Subterm (b,Some id,a) ->
+      (if b then str"appcontext " else str "context ") ++ pr_id id ++ str "[" ++ pr_pat a ++ str "]"
+
+let pr_match_hyps pr_pat = function
+  | Hyp (nal,mp) ->
+      pr_lname nal ++ str ":" ++ pr_match_pattern pr_pat mp
+  | Def (nal,mv,mp) ->
+      pr_lname nal ++ str ":=" ++ pr_match_pattern pr_pat mv
+      ++ str ":" ++ pr_match_pattern pr_pat mp
 
 let pr_match_rule m pr pr_pat = function
   | Pat ([],mp,t) when m ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 4b52772b5..e27a93b33 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -259,13 +259,16 @@ let mlexpr_of_entry_type = function
 
 let mlexpr_of_match_pattern = function
   | Tacexpr.Term t -> <:expr< Tacexpr.Term $mlexpr_of_pattern_ast t$ >>
-  | Tacexpr.Subterm (ido,t) ->
-      <:expr< Tacexpr.Subterm $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
+  | Tacexpr.Subterm (b,ido,t) ->
+      <:expr< Tacexpr.Subterm $mlexpr_of_bool b$ $mlexpr_of_option mlexpr_of_ident ido$ $mlexpr_of_pattern_ast t$ >>
 
 let mlexpr_of_match_context_hyps = function
   | Tacexpr.Hyp (id,l) ->
       let f = mlexpr_of_located mlexpr_of_name in
       <:expr< Tacexpr.Hyp $f id$ $mlexpr_of_match_pattern l$ >>
+  | Tacexpr.Def (id,v,l) ->
+      let f = mlexpr_of_located mlexpr_of_name in
+      <:expr< Tacexpr.Def $f id$ $mlexpr_of_match_pattern v$ $mlexpr_of_match_pattern l$ >>
 
 let mlexpr_of_match_rule f = function
   | Tacexpr.Pat (l,mp,t) -> <:expr< Tacexpr.Pat $mlexpr_of_list mlexpr_of_match_context_hyps l$ $mlexpr_of_match_pattern mp$ $f t$ >>