From efbc16c17d5ff8d4db80213368b43ad10fe6c461 Mon Sep 17 00:00:00 2001
From: delahaye
Date: Fri, 20 Apr 2001 08:11:23 +0000
Subject: Petit menage

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1642 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 parsing/g_tactic.ml4 | 24 ------------------------
 1 file changed, 24 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index d9a8e13189..e32a649f05 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -323,30 +323,6 @@ GEXTEND Gram
         -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
       |	IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
         <:ast< (MATCH $com ($LIST $mrl)) >>
-
-(*      | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-          <:ast<(FIRST ($LIST $l))>>
-      |	IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-          <:ast<(TCLSOLVE ($LIST $l))>>
-      | IDENT "Info"; tc = tactic_expr_par -> <:ast< (INFO $tc) >>
-      |	IDENT "Try"; ta0 = tactic_expr_par; "Orelse"; ta1 = tactic_expr_par ->
-        <:ast< (TRY (ORELSE $ta0 $ta1)) >>
-      |	IDENT "Try"; ta = tactic_expr_par -> <:ast< (TRY $ta) >>
-      | IDENT "Do"; n = pure_numarg; ta = tactic_expr_par ->
-        <:ast< (DO $n $ta) >>
-      | IDENT "Repeat"; ta = tactic_expr_par -> <:ast< (REPEAT $ta) >>
-      |	IDENT "Repeat"; ta0 = tactic_expr_par; "Orelse";
-        ta1 = tactic_expr_par ->
-        <:ast< (REPEAT (ORELSE $ta0 $ta1)) >>
-      |	IDENT "Idtac" -> <:ast< (IDTAC) >>
-      |	IDENT "Fail" -> <:ast<(FAIL)>>
-      |	IDENT "Fail"; n = pure_numarg -> <:ast<(FAIL $n)>>
-      |	st = simple_tactic -> st
-      |	st = simple_tactic; "Orelse"; ta1 = tactic_expr_par ->
-          <:ast< (ORELSE $st $ta1) >>
-      |	ta0 = tactic_expr_par; "Orelse"; ta1 = tactic_expr_par ->
-          <:ast< (ORELSE $ta0 $ta1) >>*)
-
       |	"("; te = tactic_expr; ")" -> te
       |	"("; te = tactic_expr; tel=LIST1 tactic_expr; ")" ->
         <:ast< (APP $te ($LIST tel)) >>
-- 
cgit v1.2.3