From bd7da353ea503423206e329af7a56174cb39f435 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Fri, 21 Jun 2013 21:04:00 +0000 Subject: Splitted up Genarg in four different levels: 1. Genarg itself which only defines the abstract datatypes needed. 2. Genintern, first file of interp/, defining the intern and subst functions. 3. Geninterp, first file of tactics/, defining the interp function. 4. Genprint, first file of printing/, dealing with the printers. The Genarg file has no dependency and is in lib/, so that we can put generic arguments everywhere, and in particular in ASTs. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16601 85f007b7-540e-0410-9357-904b9bb8a0f7 --- printing/genprint.mli | 28 ++++++++++++++++++++++++++++ 1 file changed, 28 insertions(+) create mode 100644 printing/genprint.mli (limited to 'printing/genprint.mli') diff --git a/printing/genprint.mli b/printing/genprint.mli new file mode 100644 index 000000000..8300f12bf --- /dev/null +++ b/printing/genprint.mli @@ -0,0 +1,28 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* 'raw -> std_ppcmds +(** Printer for raw level generic arguments. *) + +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds +(** Printer for glob level generic arguments. *) + +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds +(** Printer for top level generic arguments. *) + +val generic_raw_print : rlevel generic_argument -> std_ppcmds +val generic_glb_print : glevel generic_argument -> std_ppcmds +val generic_top_print : tlevel generic_argument -> std_ppcmds + +val register_print0 : ('raw, 'glb, 'top) genarg_type -> + ('raw -> std_ppcmds) -> ('glb -> std_ppcmds) -> ('top -> std_ppcmds) -> unit -- cgit v1.2.3