diff options
Diffstat (limited to 'syntax/PPConstr.v')
| -rwxr-xr-x | syntax/PPConstr.v | 9 |
1 files changed, 8 insertions, 1 deletions
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 *) |