This is exactly the structure needed to handle controlling printing

of terms of record type with record or constructor syntax.

Signed-off-by: Tom Prince <tom.prince@ualberta.net>

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14285 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 18 insertions, 0 deletions

diff --git a/pretyping/detyping.mli b/pretyping/detyping.mli
index ff98f747e..a423a471f 100644
--- a/pretyping/detyping.mli
+++ b/pretyping/detyping.mli
@@ -54,3 +54,21 @@ val simple_cases_matrix_of_branches :
   inductive -> int list -> glob_constr list -> cases_clauses
 val return_type_of_predicate :
   inductive -> int -> int -> glob_constr -> predicate_pattern * glob_constr option
+
+module PrintingInductiveMake :
+  functor (Test : sig
+    val encode : Libnames.reference -> Names.inductive
+    val member_message : Pp.std_ppcmds -> bool -> Pp.std_ppcmds
+    val field : string
+    val title : string
+  end) ->
+    sig
+      type t = Names.inductive
+      val encode : Libnames.reference -> Names.inductive
+      val subst : substitution -> t -> t
+      val printer : t -> Pp.std_ppcmds
+      val key : Goptions.option_name
+      val title : string
+      val member_message : t -> bool -> Pp.std_ppcmds
+      val synchronous : bool
+    end