matita/components/ng_extraction/common.mli

   1 (************************************************************************)
   2 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
   3 (* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
   4 (*   \VV/  **************************************************************)
   5 (*    //   *      This file is distributed under the terms of the       *)
   6 (*         *       GNU Lesser General Public License Version 2.1        *)
   7 (************************************************************************)
   8
   9 (*i $Id: common.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
  10
  11 open Coq
  12 open Miniml
  13 open Mlutil
  14 open OcamlExtractionTable
  15
  16 (** By default, in module Format, you can do horizontal placing of blocks
  17     even if they include newlines, as long as the number of chars in the
  18     blocks are less that a line length. To avoid this awkward situation,
  19     we attach a big virtual size to [fnl] newlines. *)
  20
  21 val fnl : unit -> std_ppcmds
  22 val space_if : bool -> std_ppcmds
  23
  24 val pp_par : bool -> std_ppcmds -> std_ppcmds
  25 val pp_apply : std_ppcmds -> bool -> std_ppcmds list -> std_ppcmds
  26 val pr_binding : identifier list -> std_ppcmds
  27
  28 type env = identifier list * Idset.t
  29 val empty_env : #OcamlExtractionTable.status -> env
  30
  31 val fake_spec: NReference.spec
  32
  33 val rename_tvars: Idset.t -> identifier list -> identifier list
  34 val push_vars : identifier list -> env -> identifier list * env
  35 val get_db_name : int -> env -> identifier
  36
  37 (* true = capitalize *)
  38 val modname_of_filename: #status as 'status-> bool -> string -> 'status * string
  39
  40 type kind = Term | Type | Cons
  41
  42 val pp_global :
  43  #status as 'status -> kind -> NReference.reference -> 'status * string