Affichage des notations récursives:

- Prise en compte des notations applicatives
- Remplacement du codage des arguments liste des notations récursives 
  sous forme de terme par une représentation directe (permet notamment
  de résoudre un problème de stack overflow de la fonction d'affichage)
+ Correction bug affichage Lemma dans ppvernac.ml
+ Divers util.ml



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

2 files changed, 4 insertions, 2 deletions

diff --git a/tactics/decl_interp.ml b/tactics/decl_interp.ml
index 2be95056e4..2701566edf 100644
--- a/tactics/decl_interp.ml
+++ b/tactics/decl_interp.ml
@@ -94,8 +94,10 @@ let rec add_vars_of_simple_pattern globs = function
 	(UserError ("simple_pattern",str "\"(_ | _)\" is not allowed here"))
   | CPatDelimiters (_,_,p) ->
       add_vars_of_simple_pattern globs p
-  | CPatCstr (_,_,pl) | CPatNotation(_,_,pl) ->
+  | CPatCstr (_,_,pl) ->
       List.fold_left add_vars_of_simple_pattern globs pl
+  | CPatNotation(_,_,(pl,pll)) ->
+      List.fold_left add_vars_of_simple_pattern globs (List.flatten (pl::pll))
   | CPatAtom (_,Some (Libnames.Ident (_,id))) -> add_var id globs
   |  _  -> globs 
 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index bbd9112d49..1e4f6a050b 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -206,7 +206,7 @@ let onHyps find tac gl = tac (find gl) gl
    after id *)
 
 let afterHyp id gl =
-  fst (list_splitby (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
+  fst (list_split_at (fun (hyp,_,_) -> hyp = id) (pf_hyps gl))
     
 
 (* Create a singleton clause list with the last hypothesis from then context *)