From 69bf012d0d2a71ed19fc89b31073747f85f9a11d Mon Sep 17 00:00:00 2001
From: delahaye
Date: Tue, 23 Oct 2001 22:40:38 +0000
Subject: Modifs Tacinterp + debugger de tactiques + syntaxe de R + DiscrR

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2136 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/PPTactic.v | 3 +++
 1 file changed, 3 insertions(+)

(limited to 'syntax')

diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index f4718f2f2b..a72a70ee57 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -418,6 +418,9 @@ Syntax tactic
                   [ $x ","[1 0] (LISTCOMA ($LIST $l)) ]
   | listcoma_one  [<<(LISTCOMA $x)>>] -> [ $x ]
   | listcoma_nil  [<<(LISTCOMA )>>] -> [ ]
+
+  (* Only when debugging *)
+  | prim_tactic [<<(PRIMTACTIC $tac)>>] -> [ $tac ]
   ;
 
   level 8:
-- 
cgit v1.2.3