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

1 files changed, 10 insertions, 6 deletions

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 ->