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
---
 parsing/g_tactic.ml4 | 4 +++-
 parsing/q_coqast.ml4 | 1 +
 2 files changed, 4 insertions(+), 1 deletion(-)

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index e370b693f0..c0a3f2e770 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -256,7 +256,9 @@ GEXTEND Gram
   naming_intropattern:
     [ [ prefix = pattern_ident -> loc, IntroFresh prefix
       | "?" -> loc, IntroAnonymous
-      | id = ident -> loc, IntroIdentifier id ] ]
+      | id = ident -> loc, IntroIdentifier id
+      | "*" -> loc, IntroForthcoming true
+      | "**" -> loc, IntroForthcoming false ] ]
   ;
   intropattern_modifier:
     [ [ IDENT "_eqn"; 
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 18322504e5..a494738f9c 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -75,6 +75,7 @@ let mlexpr_of_intro_pattern = function
   | Genarg.IntroWildcard -> <:expr< Genarg.IntroWildcard >>
   | Genarg.IntroAnonymous -> <:expr< Genarg.IntroAnonymous >>
   | Genarg.IntroFresh id -> <:expr< Genarg.IntroFresh (mlexpr_of_ident $dloc$ id) >>
+  | Genarg.IntroForthcoming b -> <:expr< Genarg.IntroForthcoming (mlexpr_of_bool $dloc$ b) >>
   | Genarg.IntroIdentifier id ->
       <:expr< Genarg.IntroIdentifier (mlexpr_of_ident $dloc$ id) >>
   | Genarg.IntroOrAndPattern _ | Genarg.IntroRewrite _ ->
-- 
cgit v1.2.3