← Back to branch summary

~ubuntu-branches/ubuntu/wily/coq-doc/wily

« back to all changes in this revision

Viewing changes to parsing/pptactic.mli

  • Committer: Bazaar Package Importer
  • Author(s): Stéphane Glondu, Stéphane Glondu, Samuel Mimram
  • Date: 2010-01-07 22:50:39 UTC
  • mfrom: (1.2.2 upstream)
  • Revision ID: james.westby@ubuntu.com-20100107225039-n3cq82589u0qt0s2
Tags: 8.2pl1-1
http://bugs.debian.org/563669
http://bugs.debian.org/543545
[ Stéphane Glondu ]
* New upstream release (Closes: #563669)
  - remove patches
* Packaging overhaul:
  - use git, advertise it in Vcs-* fields of debian/control
  - use debhelper 7 and dh with override
  - use source format 3.0 (quilt)
* debian/control:
  - set Maintainer to d-o-m, set Uploaders to Sam and myself
  - add Homepage field
  - bump Standards-Version to 3.8.3
* Register PDF documentation into doc-base
* Add debian/watch
* Update debian/copyright

[ Samuel Mimram ]
* Change coq-doc's description to mention that it provides documentation in
  pdf format, not postscript, closes: #543545.

Show diffs side-by-side

added added

removed removed

Lines of Context:
parsing/pptactic.mli
 
1
(************************************************************************)
 
2
(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
 
3
(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
 
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: pptactic.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
10
 
 
11
open Pp
 
12
open Genarg
 
13
open Tacexpr
 
14
open Pretyping
 
15
open Proof_type
 
16
open Topconstr
 
17
open Rawterm
 
18
open Ppextend
 
19
open Environ
 
20
open Evd
 
21
 
 
22
val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds
 
23
val pr_or_metaid : ('a -> std_ppcmds) -> 'a or_metaid -> std_ppcmds
 
24
val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
 
25
val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
 
26
 
 
27
type 'a raw_extra_genarg_printer =
 
28
    (constr_expr -> std_ppcmds) -> 
 
29
    (constr_expr -> std_ppcmds) -> 
 
30
    (tolerability -> raw_tactic_expr -> std_ppcmds) ->
 
31
    'a -> std_ppcmds
 
32
 
 
33
type 'a glob_extra_genarg_printer =
 
34
    (rawconstr_and_expr -> std_ppcmds) ->
 
35
    (rawconstr_and_expr -> std_ppcmds) ->
 
36
    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
 
37
    'a -> std_ppcmds
 
38
 
 
39
type 'a extra_genarg_printer =
 
40
    (Term.constr -> std_ppcmds) -> 
 
41
    (Term.constr -> std_ppcmds) -> 
 
42
    (tolerability -> glob_tactic_expr -> std_ppcmds) ->
 
43
    'a -> std_ppcmds
 
44
 
 
45
  (* if the boolean is false then the extension applies only to old syntax *)
 
46
val declare_extra_genarg_pprule : 
 
47
  ('c raw_abstract_argument_type * 'c raw_extra_genarg_printer) ->
 
48
  ('a glob_abstract_argument_type * 'a glob_extra_genarg_printer) ->
 
49
  ('b typed_abstract_argument_type * 'b extra_genarg_printer) -> unit
 
50
 
 
51
type grammar_terminals = string option list
 
52
 
 
53
  (* if the boolean is false then the extension applies only to old syntax *)
 
54
val declare_extra_tactic_pprule : 
 
55
  string * argument_type list * (int * grammar_terminals) -> unit
 
56
 
 
57
val exists_extra_tactic_pprule : string -> argument_type list -> bool
 
58
 
 
59
val pr_raw_generic : 
 
60
  (constr_expr -> std_ppcmds) ->
 
61
  (constr_expr -> std_ppcmds) ->
 
62
  (tolerability -> raw_tactic_expr -> std_ppcmds) ->
 
63
  (Libnames.reference -> std_ppcmds) -> constr_expr generic_argument ->
 
64
    std_ppcmds
 
65
 
 
66
val pr_raw_extend:
 
67
  (constr_expr -> std_ppcmds) -> (constr_expr -> std_ppcmds) ->
 
68
  (tolerability -> raw_tactic_expr -> std_ppcmds) -> int ->
 
69
    string -> raw_generic_argument list -> std_ppcmds
 
70
 
 
71
val pr_glob_extend:
 
72
  (rawconstr_and_expr -> std_ppcmds) -> (rawconstr_and_expr -> std_ppcmds) ->
 
73
  (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
 
74
    string -> glob_generic_argument list -> std_ppcmds
 
75
 
 
76
val pr_extend :
 
77
  (open_constr -> std_ppcmds) -> (open_constr -> std_ppcmds) ->
 
78
  (tolerability -> glob_tactic_expr -> std_ppcmds) -> int ->
 
79
    string -> typed_generic_argument list -> std_ppcmds
 
80
 
 
81
val pr_ltac_constant : Nametab.ltac_constant -> std_ppcmds
 
82
 
 
83
val pr_raw_tactic : env -> raw_tactic_expr -> std_ppcmds
 
84
 
 
85
val pr_raw_tactic_level : env -> tolerability -> raw_tactic_expr -> std_ppcmds
 
86
 
 
87
val pr_glob_tactic : env -> glob_tactic_expr -> std_ppcmds
 
88
 
 
89
val pr_tactic : env -> Proof_type.tactic_expr -> std_ppcmds
 
90
 
 
91
val pr_hintbases : string list option -> std_ppcmds
 
92
 
 
93
val pr_auto_using : ('constr -> std_ppcmds) -> 'constr list -> std_ppcmds
 
94
 
 
95
val pr_bindings :
 
96
  ('constr -> std_ppcmds) ->
 
97
  ('constr -> std_ppcmds) -> 'constr bindings -> std_ppcmds