From 6a13615a1efa7e2e10ea8e7187d2bda0819fd1d5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 7 Jun 2009 17:10:17 +0000
Subject: - 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
---
 interp/genarg.ml  | 3 +++
 interp/genarg.mli | 1 +
 2 files changed, 4 insertions(+)

(limited to 'interp')

diff --git a/interp/genarg.ml b/interp/genarg.ml
index 35107c8080..8724b0bfd6 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
diff --git a/interp/genarg.mli b/interp/genarg.mli
index 92c7db36f4..9072456c3e 100644
--- a/interp/genarg.mli
+++ b/interp/genarg.mli
@@ -39,6 +39,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
 
-- 
cgit v1.2.3