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 21450bf30..0adecd707 100644 --- a/parsing/prettyp.ml +++ b/parsing/prettyp.ml @@ -294,7 +294,7 @@ let print_inductive sp = (print_mutual sp ++ fnl ()) let print_syntactic_def sep sp = let id = basename sp in let c = Syntax_def.search_syntactic_definition sp in - (str" Syntactif Definition " ++ pr_id id ++ str sep ++ pr_rawterm c ++ fnl ()) + (str" Syntactic Definition " ++ pr_id id ++ str sep ++ pr_rawterm c ++ fnl ()) let print_leaf_entry with_values sep (sp,lobj) = let tag = object_tag lobj in |