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

1 files changed, 8 insertions, 1 deletions

diff --git a/syntax/PPConstr.v b/syntax/PPConstr.v
index 4980afd58..ad74cd462 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 *)