From 424bf8a5131aaf4960745c7050e5977c6e5fd4a5 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 7 Jan 2000 22:27:11 +0000
Subject: Renommage command en constr

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@267 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 syntax/MakeBare.v | 4 ++--
 syntax/PPTactic.v | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'syntax')

diff --git a/syntax/MakeBare.v b/syntax/MakeBare.v
index 8740d5a04d..bb12e70585 100644
--- a/syntax/MakeBare.v
+++ b/syntax/MakeBare.v
@@ -1,3 +1,3 @@
-Load PPCommand.
-Load PPTactic.
+Load PPConstr.
 Load PPCases.
+Load PPTactic.
diff --git a/syntax/PPTactic.v b/syntax/PPTactic.v
index 62c3319a0c..e9a5f11b54 100644
--- a/syntax/PPTactic.v
+++ b/syntax/PPTactic.v
@@ -312,4 +312,4 @@ Syntax tactic
   ;
 
   level 8:
-  command [(COMMAND $c)] -> [ (PPUNI$COMMAND $c):E ].
+  tactic_to_constr [(COMMAND $c)] -> [ $c:"constr":9 ].
-- 
cgit v1.2.3