- Added two new introduction patterns with the following temptative syntaxes:

  - "*" implements Arthur Charguéraud's "introv"
  - "**" works as "; intros" (see also "*" in ssreflect).
- Simplifying the proof of Z_eq_dec, as suggested by Frédéric Blanqui.
- Shy attempt to seize the opportunity to clean Zarith_dec but Coq's
  library is really going anarchically (see a summary of the various
  formulations of total order, dichotomy of order and decidability of
  equality and in stdlib-project.tex in branch V8revised-theories).



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

1 files changed, 3 insertions, 0 deletions

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 35107c808..8724b0bfd 100644
--- a/interp/genarg.ml
+++ b/interp/genarg.ml
@@ -82,6 +82,7 @@ type intro_pattern_expr =
   | IntroRewrite of bool
   | IntroIdentifier of identifier
   | IntroFresh of identifier
+  | IntroForthcoming of bool
   | IntroAnonymous
 and or_and_intro_pattern_expr = (loc * intro_pattern_expr) list list
 
@@ -92,6 +93,8 @@ let rec pr_intro_pattern (_,pat) = match pat with
   | IntroRewrite false -> str "<-"
   | IntroIdentifier id -> pr_id id
   | IntroFresh id -> str "?" ++ pr_id id
+  | IntroForthcoming true -> str "*"
+  | IntroForthcoming false -> str "**"
   | IntroAnonymous -> str "?"
 
 and pr_or_and_intro_pattern = function