From cfb4d4e05fe41dda9507372f31b8ced11d3f2fe4 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 23 May 2000 19:34:48 +0000
Subject: Réparation bug d'affichage et affichage des instanciations par des
 {...}

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

(limited to 'syntax/PPConstr.v')

diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 4980afd587..ad74cd462e 100755
--- a/syntax/PPConstr.v
+++ b/syntax/PPConstr.v
@@ -35,12 +35,19 @@ Syntax constr
   | type [(TYPE)] -> ["Type"]
   | type_sp [(TYPE ($PATH $sp) ($NUM $n))] -> ["Type"]
 (* Note: Atomic constants (Nvar, CONST, MUTIND, MUTCONSTRUCT) are printed in
-   typing/printer to deal with the duality CCI/FW *)
+   Printer to know if they must be qualified or not (and previously to
+   deal with the duality CCI/FW) *)
 
   | evar [<< ? >>] -> ["?"]
   | meta [(META ($NUM $n))] -> [ "?" $n ]
   | implicit [(IMPLICIT)] -> ["<Implicit>"]
   | indice [(REL ($NUM $n))] -> ["<Unbound ref: " $n ">"]
+  | instantiation [(INSTANCE $a ($LIST $l))] ->
+	 [ $a "{" (CONTEXT ($LIST $l)) "}"]
+  | instantiation_nil [(CONTEXT)] -> [ ]
+  | instantiation_one [(CONTEXT $a)] -> [ $a ]
+  | instantiation_many [(CONTEXT $a $b ($LIST $l))] ->
+	 [ (CONTEXT $b ($LIST $l)) ";" $a ]
   ;
 
 (* Things parsed in command1 *)
-- 
cgit v1.2.3