From f5a8095075c8677efe5ee89b1d7ec53b1b10082b Mon Sep 17 00:00:00 2001 From: herbelin Date: Thu, 19 Oct 2006 07:46:03 +0000 Subject: coqide: affichage des sous-buts et hypothèses et métas comme types de telle sorte que les coercions vers sortclass ne soient pas affichées (comme dans coqtop) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9249 85f007b7-540e-0410-9357-904b9bb8a0f7 --- parsing/printer.mli | 1 + 1 file changed, 1 insertion(+) (limited to 'parsing') diff --git a/parsing/printer.mli b/parsing/printer.mli index c63d7d71f..dd2a7bad0 100644 --- a/parsing/printer.mli +++ b/parsing/printer.mli @@ -35,6 +35,7 @@ val pr_lconstr : constr -> std_ppcmds val pr_constr_env : env -> constr -> std_ppcmds val pr_constr : constr -> std_ppcmds +val pr_ltype_env_at_top : env -> types -> std_ppcmds val pr_ltype_env : env -> types -> std_ppcmds val pr_ltype : types -> std_ppcmds -- cgit v1.2.3