diff options
| -rw-r--r-- | parsing/prettyp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/parsing/prettyp.ml b/parsing/prettyp.ml index fc31d1d26e..baa65c40ef 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -461,7 +461,7 @@ let print_about ref = let k = locate_any_name ref in begin match k with | Term (ConstRef sp as ref) -> - print_constant false " = " sp + print_constant false " : " sp | Term (IndRef ind as ref) -> let ty = Inductive.type_of_inductive env ind in print_typed_value (mkInd ind, ty) ++ |