Add occurence extra arg

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

2 files changed, 15 insertions, 0 deletions

diff --git a/tactics/extraargs.ml4 b/tactics/extraargs.ml4
index 48d4afbc1..1d9d5e0e9 100644
--- a/tactics/extraargs.ml4
+++ b/tactics/extraargs.ml4
@@ -33,6 +33,17 @@ ARGUMENT EXTEND orient TYPED AS bool PRINTED BY pr_orient
 | [ ] -> [ true ]
 END
 
+let pr_occurences _prc _prlc _prt l =
+  let rec aux = function
+    | i :: l -> Pp.int i ++ Pp.spc () ++ aux l
+    | [] -> Pp.mt()
+  in aux l
+
+ARGUMENT EXTEND occurences TYPED AS int list PRINTED BY pr_occurences
+| [ integer(i) occurences(l) ] -> [ i :: l ]
+| [ ] -> [ [] ]
+END
+
 (* For Setoid rewrite *)
 let pr_morphism_signature _ _ _ s =
   spc () ++ Setoid_replace.pr_morphism_signature s
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 2f891a61f..ead64ac3b 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -19,6 +19,10 @@ val rawwit_orient : bool raw_abstract_argument_type
 val wit_orient : bool typed_abstract_argument_type
 val orient : bool Pcoq.Gram.Entry.e
 
+val rawwit_occurences : (int list) raw_abstract_argument_type
+val wit_occurences : (int list) typed_abstract_argument_type
+val occurences : (int list) Pcoq.Gram.Entry.e
+
 val rawwit_morphism_signature :
  Setoid_replace.morphism_signature raw_abstract_argument_type
 val wit_morphism_signature :