Découpage de g_tactic.ml4 en 2 (pour satisfaire les contraintes de la compilation native powerpc), le nouveau morceau étant g_ltac.ml4

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

1 files changed, 1 insertions, 145 deletions

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 42552fbd15..70aaba18d1 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -227,146 +227,7 @@ GEXTEND Gram
   ;
  END
 
-(* Tactics grammar rules *)
-
 GEXTEND Gram
-  input_fun:
-    [ [ l = identarg -> l
-      | "()" -> <:ast< (VOID) >> ] ]
-  ;
-  let_clause:
-    [ [ id = identarg; "="; te=tactic_atom -> <:ast< (LETCLAUSE $id $te) >>
-      | id = identarg; ":"; c = constrarg; ":="; "Proof" ->
-        (match c with
-        | Coqast.Node(_,"COMMAND",[csr]) ->
-          <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
-	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">])
-      | id = identarg; ":"; c = constrarg; ":="; te = tactic_expr ->
-        <:ast< (LETCUTCLAUSE $id $c $te) >> 
-      |	id = identarg; ":"; c = constrarg ->
-        (match c with
-        | Coqast.Node(_,"COMMAND",[csr]) ->
-          <:ast< (LETTOPCLAUSE $id (CONSTR $csr)) >>
-	| _ -> errorlabstrm "Gram.let_clause" [<'sTR "Not a COMMAND">]) ] ]
-  ;
-  rec_clause:
-    [ [ name = identarg; it = LIST1 input_fun; "->"; body = tactic_atom ->
-          <:ast< (RECCLAUSE $name (FUNVAR ($LIST $it)) $body) >> ] ]
-  ;
-  match_pattern:
-    [ [ id = constrarg; "["; pc = constrarg; "]" ->
-        (match id with
-        | Coqast.Node(_,"COMMAND",
-            [Coqast.Node(_,"QUALID",[Coqast.Nvar(_,s)])]) ->
-          <:ast< (SUBTERM ($VAR $s) $pc) >>
-        | _ ->
-          errorlabstrm "Gram.match_pattern" [<'sTR "Not a correct SUBTERM">])
-      | "["; pc = constrarg; "]" -> <:ast< (SUBTERM $pc) >>
-      | pc = constrarg -> <:ast< (TERM $pc) >> ] ]
-  ;
-  match_hyps:
-    [ [ id = identarg; ":"; mp =  match_pattern ->
-          <:ast< (MATCHCONTEXTHYPS $id $mp) >>
-      | IDENT "_"; ":"; mp = match_pattern ->
-          <:ast< (MATCHCONTEXTHYPS $mp) >> ] ]
-  ;
-  match_context_rule:
-    [ [ "["; largs = LIST0 match_hyps SEP ";"; "|-"; mp = match_pattern; "]";
-        "->"; te = tactic_expr ->
-            <:ast< (MATCHCONTEXTRULE ($LIST $largs) $mp $te) >> 
-      | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHCONTEXTRULE $te) >>
-    ] ]
-  ;
-  match_context_list:
-    [ [ mrl = LIST1 match_context_rule SEP "|" -> mrl
-      | "|"; mrl = LIST1 match_context_rule SEP "|" -> mrl ] ]
-  ;
-  match_rule:
-    [ [ "["; mp = match_pattern; "]"; "->"; te = tactic_expr ->
-        <:ast<(MATCHRULE $mp $te)>>
-      | IDENT "_"; "->"; te = tactic_expr -> <:ast< (MATCHRULE $te) >> ] ]
-  ;
-  match_list:
-    [ [ mrl = LIST1 match_rule SEP "|" -> mrl
-      | "|"; mrl = LIST1 match_rule SEP "|" -> mrl ] ]
-  ;
-  tactic_expr:
-    [ [ ta0 = tactic_expr; ";"; ta1 = tactic_expr ->
-         <:ast< (TACTICLIST $ta0 $ta1) >>
-      | ta = tactic_expr; ";"; "["; lta = LIST0 tactic_expr SEP "|"; "]" ->
-         <:ast< (TACTICLIST $ta (TACLIST ($LIST $lta))) >>
-      | y = tactic_atom0 -> y ] ]
-  ;
-  tactic_atom0:
-    [ [ la = LIST1 tactic_atom ->
-        if (List.length la) = 1 then
-          let el = List.hd la in <:ast< $el >>
-        else
-          <:ast< (APP ($LIST $la)) >> ] ]
-  ;
-  tactic_atom:
-    [ [ IDENT "Fun"; it = LIST1 input_fun ; "->"; body = tactic_expr ->
-          <:ast< (FUN (FUNVAR ($LIST $it)) $body) >>
-      | IDENT "Rec"; rc = rec_clause -> <:ast< (REC $rc) >>
-      |	IDENT "Rec"; rc = rec_clause; IDENT "In"; body = tactic_expr ->
-          <:ast< (REC (RECDECL $rc) $body) >>
-      | IDENT "Rec"; rc = rec_clause; "And";
-          rcl = LIST1 rec_clause SEP "And"; IDENT "In";
-          body = tactic_expr ->
-            <:ast< (REC (RECDECL $rc ($LIST $rcl)) $body) >>
-      | IDENT "Let"; llc = LIST1 let_clause SEP "And"; IDENT "In";
-          u = tactic_expr -> <:ast< (LET (LETDECL ($LIST $llc)) $u) >>
-      |	IDENT "Let"; llc = LIST1 let_clause SEP "And" ->
-        (match llc with
-	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
-          <:ast< (StartProof "LETTOP" $id $c) >>
-        | _ -> <:ast< (LETCUT (LETDECL ($LIST $llc))) >>)
-      |	IDENT "Let"; llc = LIST1 let_clause SEP "And";
-        tb = Vernac_.theorem_body; "Qed" ->
-        (match llc with
-	| [Coqast.Node(_,"LETTOPCLAUSE",[id;c])] ->
-          <:ast< (TheoremProof "LETTOP" $id $c $tb) >>
-	| _ -> errorlabstrm "Gram.tactic_atom" [<'sTR "Not a LETTOPCLAUSE">])
-      |	IDENT "Match"; IDENT "Context"; IDENT "With"; mrl = match_context_list
-        -> <:ast< (MATCHCONTEXT ($LIST $mrl)) >>
-      |	IDENT "Match"; com = constrarg; IDENT "With"; mrl = match_list ->
-        <:ast< (MATCH $com ($LIST $mrl)) >>
-      |	"("; te = tactic_expr; ")" -> te
-      |	"("; te = tactic_expr; tel=LIST1 tactic_expr; ")" ->
-        <:ast< (APP $te ($LIST tel)) >>
-      | IDENT "First" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-          <:ast<(FIRST ($LIST $l))>>
-      | IDENT "Info"; tc = tactic_expr -> <:ast< (INFO $tc) >>
-      |	IDENT "Solve" ; "["; l = LIST0 tactic_expr SEP "|"; "]" ->
-          <:ast<(TCLSOLVE ($LIST $l))>>
-      |	IDENT "Try"; ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
-        <:ast< (TRY (ORELSE $ta0 $ta1)) >>
-      |	IDENT "Try"; ta = tactic_atom -> <:ast< (TRY $ta) >>
-      | IDENT "Do"; n = pure_numarg; ta = tactic_atom -> <:ast< (DO $n $ta) >>
-      |	IDENT "Repeat"; ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
-        <:ast< (REPEAT (ORELSE $ta0 $ta1)) >>
-      | IDENT "Repeat"; ta = tactic_atom -> <:ast< (REPEAT $ta) >>
-      |	IDENT "Idtac" -> <:ast< (IDTAC) >>
-      |	IDENT "Fail" -> <:ast<(FAIL)>>
-      |	IDENT "Fail"; n = pure_numarg -> <:ast<(FAIL $n)>>
-      |	ta0 = tactic_atom; "Orelse"; ta1 = tactic_atom ->
-          <:ast< (ORELSE $ta0 $ta1) >>
-      | IDENT "Progress"; ta = tactic_atom -> <:ast< (PROGRESS $ta) >>
-      |	st = simple_tactic -> st
-      |	tca = tactic_arg -> tca ] ]
-  ;
-  tactic_arg:
-    [ [ "()" -> <:ast< (VOID) >>
-      | n = pure_numarg -> n
-      |	id = identarg -> id
-      |	"?" -> <:ast< (COMMAND (ISEVAR)) >>
-      | "?"; n = Prim.number -> <:ast< (COMMAND (META $n)) >>
-      |	IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
-        <:ast< (COMMAND (EVAL $c (REDEXP $rtc))) >>
-      | IDENT "Inst"; id = identarg; "["; c = Constr.constr; "]" ->
-        <:ast< (COMMAND (CONTEXT $id $c)) >>
-      |	"'"; c = constrarg -> c ] ]
-  ;
   simple_tactic:
     [ [ IDENT "Fix"; n = pure_numarg -> <:ast< (Fix $n) >>
       | IDENT "Fix"; id = identarg; n = pure_numarg -> <:ast< (Fix $id $n) >>
@@ -407,12 +268,7 @@ GEXTEND Gram
       | IDENT "Auto"; IDENT "Decomp" -> <:ast< (DAuto) >>
       | IDENT "Auto"; n = pure_numarg; IDENT "Decomp"; p = pure_numarg ->
           <:ast< (DAuto $n $p) >>
-      ] ];
-    END
-
-GEXTEND Gram
- simple_tactic:
-  [ [  IDENT "Intros" -> <:ast< (Intros) >>
+      | IDENT "Intros" -> <:ast< (Intros) >>
       | IDENT "Intros"; IDENT "until"; id = identarg 
                                               -> <:ast< (IntrosUntil $id) >>
       | IDENT "Intros"; IDENT "until"; n = numarg -> <:ast<(IntrosUntil $n)>>