From d21d934c5ef9f47046a705eebd554e63f77b9e30 Mon Sep 17 00:00:00 2001
From: filliatr
Date: Mon, 13 Dec 1999 15:23:16 +0000
Subject:  - états fabriqués avec -silent  - compilation theories avec -q  -
 correction but de tclORELSE qui doit maintenant rattraper aussi    TypeError
 et RefinerError

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

(limited to 'parsing')

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 0548788e6e..586a1bd67d 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -129,7 +129,6 @@ GEXTEND Gram
       | IDENT "Unfold"; ul = ne_unfold_occ_list ->
           <:ast< (Unfold ($LIST ul)) >>
       | IDENT "Fold"; cl = comarg_list -> <:ast< (Fold ($LIST cl)) >>
-      | IDENT "Change"; c = comarg -> <:ast< (Change $c) >>
       | IDENT "Pattern"; pl = ne_pattern_list ->
           <:ast< (Pattern ($LIST $pl)) >> ] ]
   ;
@@ -306,7 +305,10 @@ GEXTEND Gram
       | IDENT "Idtac" -> <:ast< (Idtac) >>
       | IDENT "Fail" -> <:ast< (Fail) >>
       | "("; tcl = tactic_com_list; ")" -> tcl
-      | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >> ]
+      | r = red_tactic; cl = clausearg -> <:ast< (Reduce (REDEXP $r) $cl) >>
+      (* Change ne doit pas s'appliquer dans un Definition t := Eval ... *)
+      | IDENT "Change"; c = comarg; cl = clausearg ->
+	  <:ast< (Change $c $cl) >> ]
 
     | [ id = identarg; l = comarg_list ->
           match (isMeta (nvar_of_ast id), l) with
-- 
cgit v1.2.3