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

12 files changed, 172 insertions, 69 deletions

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index 7d1f57fe19..07cc101889 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -643,12 +643,14 @@ let is_tactic_special_case = function
 let xlate_context_pattern = function
   | Term v -> 
       CT_coerce_FORMULA_to_CONTEXT_PATTERN (xlate_formula v)
-  | Subterm (idopt, v) ->
+  | Subterm (b, idopt, v) -> (* TODO: application pattern *)
       CT_context(xlate_ident_opt idopt, xlate_formula v)
 
 
 let xlate_match_context_hyps = function
-  | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b);;
+  | Hyp (na,b) -> CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b)
+  | Def (na,b,t) -> xlate_error "TODO: Let hyps"
+      (* CT_premise_pattern(xlate_id_opt na, xlate_context_pattern b, xlate_context_pattern t);; *)
 
 let xlate_arg_to_id_opt = function
     Some id -> CT_coerce_ID_to_ID_OPT(CT_ident (string_of_id id))
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index cd10e51f15..d9bc8038b9 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 e59df48aa5..3d1eec4fe1 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 4b52772b5b..e27a93b33e 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$ >>
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 *)
 
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 1808fd3aac..f3152f3314 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -117,11 +117,12 @@ type pattern_expr = constr_expr
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
-  | Subterm of identifier option * 'a
+  | Subterm of bool * identifier option * 'a
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
   | Hyp of name located * 'a match_pattern
+  | Def of name located * 'a match_pattern * 'a match_pattern
 
 (* Type of a Match rule for Match Context and Match *)
 type ('a,'t) match_rule =
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 16bca302e7..6674d04ea9 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id:$ i*)
+(*i $Id$ i*)
 
 open Names
 open Constrextern
@@ -129,7 +129,7 @@ let hyp_bound = function
   | Name id -> " (bound to "^(Names.string_of_id id)^")"
 
 (* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,c) ido =
+let db_matched_hyp debug env (id,_,c) ido =
   if debug <> DebugOff & !skip = 0 then
     msgnl (str "Hypothesis " ++
            str ((Names.string_of_id id)^(hyp_bound ido)^
@@ -148,8 +148,8 @@ let db_mc_pattern_success debug =
 
 let pp_match_pattern env = function
   | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
-  | Subterm (o,c) ->
-    Subterm (o,(extern_constr_pattern (names_of_rel_context env) c))
+  | Subterm (b,o,c) ->
+    Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c))
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 6da6dc61cf..ab59f208af 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -45,7 +45,7 @@ val db_pattern_rule :
 
 (* Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> identifier * constr -> name -> unit
+  debug_info -> env -> identifier * constr option * constr -> name -> unit
 
 (* Prints the matched conclusion *)
 val db_matched_concl : debug_info -> env -> constr -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2fc6692a8f..309aef8076 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -135,9 +135,6 @@ let rec pr_value env = function
   | VList (a::_) ->
       str "a list (first element is " ++ pr_value env a ++ str")"
 
-(* Transforms a named_context into a (string * constr) list *)
-let make_hyps = List.map (fun (id,_,typ) -> (id, typ))
-
 (* Transforms an id into a constr if possible, or fails *)
 let constr_of_id env id = 
   construct_reference (Environ.named_context env) id
@@ -620,9 +617,9 @@ let interp_constrpattern_gen sigma env ?(as_type=false) ltacvar c =
 
 (* Reads a pattern *)
 let intern_pattern sigma env ?(as_type=false) lfun = function
-  | Subterm (ido,pc) ->
+  | Subterm (b,ido,pc) ->
       let (metas,pat) = interp_constrpattern_gen sigma env lfun pc in
-      ido, metas, Subterm (ido,pat)
+      ido, metas, Subterm (b,ido,pat)
   | Term pc ->
       let (metas,pat) = interp_constrpattern_gen sigma env ~as_type lfun pc  in
       None, metas, Term pat
@@ -659,6 +656,12 @@ let rec intern_match_context_hyps sigma env lfun = function
       let lfun, metas2, hyps = intern_match_context_hyps sigma env lfun tl in
       let lfun' = name_cons na (Option.List.cons ido lfun) in
       lfun', metas1@metas2, Hyp (locna,pat)::hyps
+  | (Def ((_,na) as locna,mv,mp))::tl ->
+      let ido, metas1, patv = intern_pattern sigma env ~as_type:false lfun mv in
+      let ido', metas2, patt = intern_pattern sigma env ~as_type:true lfun mp in
+      let lfun, metas3, hyps = intern_match_context_hyps sigma env lfun tl in
+      let lfun' = name_cons na (Option.List.cons ido' (Option.List.cons ido lfun)) in
+      lfun', metas1@metas2@metas3, Def (locna,patv,patt)::hyps
   | [] -> lfun, [], []
 
 (* Utilities *)
@@ -1000,7 +1003,7 @@ let eval_pattern lfun c =
   instantiate_pattern lvar c
 
 let read_pattern lfun = function
-  | Subterm (ido,pc) -> Subterm (ido,eval_pattern lfun pc)
+  | Subterm (b,ido,pc) -> Subterm (b,ido,eval_pattern lfun pc)
   | Term pc -> Term (eval_pattern lfun pc)
 
 (* Reads the hypotheses of a Match Context rule *)
@@ -1016,6 +1019,10 @@ let rec read_match_context_hyps lfun lidh = function
       let lidh' = name_fold cons_and_check_name na lidh in
       Hyp (locna,read_pattern lfun mp)::
 	(read_match_context_hyps lfun lidh' tl)
+  | (Def ((loc,na) as locna,mv,mp))::tl ->
+      let lidh' = name_fold cons_and_check_name na lidh in
+      Def (locna,read_pattern lfun mv, read_pattern lfun mp)::
+	(read_match_context_hyps lfun lidh' tl)
   | [] -> []
 
 (* Reads the rules of a Match Context or a Match *)
@@ -1043,37 +1050,69 @@ let rec verify_metas_coherence gl lcm = function
       raise Not_coherent_metas
   | [] -> []
 
+type match_result = 
+  | Matches of (Names.identifier * value) list * (Rawterm.patvar * Term.constr) list *
+      (int * bool)
+  | Fail of int * bool
+
 (* Tries to match one hypothesis pattern with a list of hypotheses *)
-let apply_one_mhyp_context ist env gl lmatch (hypname,pat) (lhyps,nocc) =
+let apply_one_mhyp_context ist env gl lmatch (hypname,patv,pat) (lhyps,nocc) =
   let get_id_couple id = function
     | Name idpat -> [idpat,VConstr (mkVar id)]
     | Anonymous -> [] in
-  let rec apply_one_mhyp_context_rec nocc = function
-    | (id,hyp)::tl as hyps ->
-      (match pat with
-      | Term t ->
+  let match_pat lmatch nocc id hyp pat =
+    match pat with
+    | Term t ->
         (try
-          let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
-          (get_id_couple id hypname,lmeta,(id,hyp),(tl,0))
-        with
-	| PatternMatchingFailure | Not_coherent_metas ->
-            apply_one_mhyp_context_rec 0 tl)
-      | Subterm (ic,t) ->
+            let lmeta = verify_metas_coherence gl lmatch (matches t hyp) in
+              Matches ([],lmeta,(0, true))
+          with
+	  | PatternMatchingFailure | Not_coherent_metas ->
+              Fail (0, true))
+    | Subterm (b,ic,t) ->
         (try
-          let (lm,ctxt) = match_subterm nocc t hyp in
+          let (lm,ctxt) = 
+	    if b then match_appsubterm nocc t hyp else match_subterm nocc t hyp 
+	  in
           let lmeta = verify_metas_coherence gl lmatch lm in
-          ((get_id_couple id hypname)@(give_context ctxt ic),
-	   lmeta,(id,hyp),(hyps,nocc + 1))
-         with
-         | PatternMatchingFailure ->
-             apply_one_mhyp_context_rec 0 tl
-         | Not_coherent_metas ->
-             apply_one_mhyp_context_rec (nocc + 1) hyps))
+            Matches 
+	      (give_context ctxt ic,lmeta,(nocc + 1,false))
+          with
+          | PatternMatchingFailure ->
+	      Fail (0, true)
+          | Not_coherent_metas ->
+              Fail (nocc + 1, false))
+  in
+  let rec apply_one_mhyp_context_rec nocc = function
+    | (id,b,hyp as hd)::tl as hyps ->
+	(match patv with
+	| None -> 
+	    (match match_pat lmatch nocc id hyp pat with
+	    | Matches (ids, lmeta, (nocc, cont)) ->
+		(get_id_couple id hypname@ids,
+		lmeta,hd,((if cont then tl else hyps),nocc))
+	    | Fail (nocc, cont) ->
+		apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+	| Some patv -> 
+	    (match b with
+	    | Some body -> 
+		(match match_pat lmatch nocc id body patv with
+		| Matches (ids, lmeta, (noccv, cont)) ->
+		    (match match_pat (lmatch@lmeta) nocc id hyp pat with
+		    | Matches (ids', lmeta', (nocc', cont')) ->
+			(get_id_couple id hypname@ids@ids',
+			lmeta@lmeta',hd,((if cont || cont' then tl else hyps),nocc'))
+		    | Fail (nocc, cont) ->
+			apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+		| Fail (nocc, cont) ->
+		    apply_one_mhyp_context_rec nocc (if cont then tl else hyps))
+	    | None -> 
+		apply_one_mhyp_context_rec nocc tl))
     | [] ->
         db_hyp_pattern_failure ist.debug env (hypname,pat);
         raise PatternMatchingFailure
-      in
-  apply_one_mhyp_context_rec nocc lhyps
+  in
+    apply_one_mhyp_context_rec nocc lhyps
 
 let constr_to_id loc = function
   | VConstr c when isVar c -> destVar c
@@ -1815,12 +1854,13 @@ and interp_letin ist gl llc u =
 
 (* Interprets the Match Context expressions *)
 and interp_match_context ist g lz lr lmr =
-  let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps =
-    let (lgoal,ctxt) = match_subterm nocc c csr in
+  let rec apply_goal_sub app ist env goal nocc (id,c) csr mt mhyps hyps =
+    let (lgoal,ctxt) = if app then match_appsubterm nocc c csr
+      else match_subterm nocc c csr in
     let lctxt = give_context ctxt id in
       try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps
       with e when is_match_catchable e ->
-	apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
+	apply_goal_sub app ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in
   let rec apply_match_context ist env goal nrs lex lpt = 
     begin
       if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex);
@@ -1833,7 +1873,7 @@ and interp_match_context ist g lz lr lmr =
 		apply_match_context ist env goal (nrs+1) (List.tl lex) tl
 	    end
 	| (Pat (mhyps,mgoal,mt))::tl ->
-	    let hyps = make_hyps (pf_hyps goal) in
+	    let hyps = pf_hyps goal in
 	    let hyps = if lr then List.rev hyps else hyps in
 	    let mhyps = List.rev mhyps (* Sens naturel *) in
 	    let concl = pf_concl goal in
@@ -1849,8 +1889,8 @@ and interp_match_context ist g lz lr lmr =
 			   | Eval_fail s -> db_eval_failure ist.debug s
 			   | _ -> db_logic_failure ist.debug e);
 			apply_match_context ist env goal (nrs+1) (List.tl lex) tl)
-		 | Subterm (id,mg) ->
-		     (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
+		 | Subterm (b,id,mg) ->
+		     (try apply_goal_sub b ist env goal 0 (id,mg) concl mt mhyps hyps
 		      with
 			| PatternMatchingFailure ->
 			    apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
@@ -1868,9 +1908,14 @@ and interp_match_context ist g lz lr lmr =
 (* Tries to match the hypotheses in a Match Context *)
 and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps =
   let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
-    | Hyp ((_,hypname),mhyp)::tl as mhyps ->
+    | hyp::tl as mhyps ->
+	let (hypname, mbod, mhyp) = 
+	  match hyp with
+	  | Hyp ((_,hypname),mhyp) -> hypname, None, mhyp
+	  | Def ((_,hypname),mbod,mhyp) -> hypname, Some mbod, mhyp
+	in
         let (lids,lm,hyp_match,next) =
-          apply_one_mhyp_context ist env goal lmatch (hypname,mhyp) current in
+          apply_one_mhyp_context ist env goal lmatch (hypname,mbod,mhyp) current in
         db_matched_hyp ist.debug (pf_env goal) hyp_match hypname;
         begin 
 	  try
@@ -1977,13 +2022,16 @@ and interp_genarg_var_list1 ist gl x =
 
 (* Interprets the Match expressions *)
 and interp_match ist g lz constr lmr =
-  let rec apply_match_subterm ist nocc (id,c) csr mt =
-    let (lm,ctxt) = match_subterm nocc c csr in
+  let rec apply_match_subterm app ist nocc (id,c) csr mt =
+    let (lm,ctxt) = 
+      if app then match_appsubterm nocc c csr 
+      else match_subterm nocc c csr 
+    in
     let lctxt = give_context ctxt id in
     let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
     try eval_with_fail {ist with lfun=lm@lctxt@ist.lfun} lz g mt
     with e when is_match_catchable e ->
-      apply_match_subterm ist (nocc + 1) (id,c) csr mt
+      apply_match_subterm app ist (nocc + 1) (id,c) csr mt
   in
   let rec apply_match ist csr = function
     | (All t)::_ ->
@@ -2010,8 +2058,8 @@ and interp_match ist g lz constr lmr =
            debugging_step ist (fun () -> str "switching to the next rule");
            apply_match ist csr tl)
 
-    | (Pat ([],Subterm (id,c),mt))::tl ->
-        (try apply_match_subterm ist 0 (id,c) csr mt
+    | (Pat ([],Subterm (b,id,c),mt))::tl ->
+        (try apply_match_subterm b ist 0 (id,c) csr mt
          with PatternMatchingFailure -> apply_match ist csr tl)
     | _ ->
       errorlabstrm "Tacinterp.apply_match" (str
@@ -2419,13 +2467,16 @@ let subst_raw_may_eval subst = function
   | ConstrTerm c -> ConstrTerm (subst_rawconstr subst c)
 
 let subst_match_pattern subst = function
-  | Subterm (ido,pc) -> Subterm (ido,subst_pattern subst pc)
+  | Subterm (b,ido,pc) -> Subterm (b,ido,subst_pattern subst pc)
   | Term pc -> Term (subst_pattern subst pc)
 
 let rec subst_match_context_hyps subst = function
   | Hyp (locs,mp) :: tl ->
       Hyp (locs,subst_match_pattern subst mp)
       :: subst_match_context_hyps subst tl
+  | Def (locs,mv,mp) :: tl ->
+      Def (locs,subst_match_pattern subst mv, subst_match_pattern subst mp)
+      :: subst_match_context_hyps subst tl
   | [] -> []
 
 let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 009e4dd11a..067af63f2b 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -66,7 +66,7 @@ let is_tactic =
       "simpl"; "unfold"; "red"; "compute"; "at"; "in"; "by";
       "reflexivity"; "symmetry"; "transitivity";
       "replace"; "setoid_replace"; "inversion"; "inversion_clear";
-      "pattern"; "intuition"; "congruence";
+      "pattern"; "intuition"; "congruence"; "fail"; "fresh";
       "trivial"; "exact"; "tauto"; "firstorder"; "ring";
       "clapply"; "program_simpl"; "eapply"; "auto"; "eauto" ]
 
diff --git a/tools/coqdoc/pretty.mll b/tools/coqdoc/pretty.mll
index d5d8702bcc..36ed0472b2 100644
--- a/tools/coqdoc/pretty.mll
+++ b/tools/coqdoc/pretty.mll
@@ -170,11 +170,12 @@ let firstchar =
   ['A'-'Z' 'a'-'z' '_' 
   (* iso 8859-1 accents *) 
   '\192'-'\214' '\216'-'\246' '\248'-'\255' ] |
+  (* *)
   '\194' '\185' |
   (* utf-8 latin 1 supplement *) 
   '\195' ['\128'-'\191'] |
   (* utf-8 letterlike symbols *) 
-  '\206' ['\177'-'\183'] |
+  '\206' ('\160' | [ '\177'-'\183'] | '\187') |
   '\226' ('\130' [ '\128'-'\137' ] (* subscripts *)
     | '\129' [ '\176'-'\187' ] (* superscripts *)
     | '\132' ['\128'-'\191'] | '\133' ['\128'-'\143'])