← Back to branch summary

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

« back to all changes in this revision

Viewing changes to contrib/subtac/subtac_utils.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:
contrib/subtac/subtac_utils.mli
 
1
open Term
 
2
open Libnames
 
3
open Coqlib
 
4
open Environ
 
5
open Pp
 
6
open Evd
 
7
open Decl_kinds
 
8
open Topconstr
 
9
open Rawterm
 
10
open Util
 
11
open Evarutil
 
12
open Names
 
13
open Sign
 
14
 
 
15
val ($) : ('a -> 'b) -> 'a -> 'b
 
16
val contrib_name : string
 
17
val subtac_dir : string list
 
18
val fix_sub_module : string
 
19
val fixsub_module : string list
 
20
val init_constant : string list -> string -> constr
 
21
val init_reference : string list -> string -> global_reference
 
22
val fixsub : constr lazy_t
 
23
val well_founded_ref : global_reference lazy_t
 
24
val acc_ref : global_reference lazy_t
 
25
val acc_inv_ref : global_reference lazy_t
 
26
val fix_sub_ref : global_reference lazy_t
 
27
val fix_measure_sub_ref : global_reference lazy_t
 
28
val lt_ref : global_reference lazy_t
 
29
val lt_wf_ref : global_reference lazy_t
 
30
val refl_ref : global_reference lazy_t
 
31
val sig_ref : reference
 
32
val proj1_sig_ref : reference
 
33
val proj2_sig_ref : reference
 
34
val build_sig : unit -> coq_sigma_data
 
35
val sig_ : coq_sigma_data lazy_t
 
36
 
 
37
val eq_ind : constr lazy_t
 
38
val eq_rec : constr lazy_t
 
39
val eq_rect : constr lazy_t
 
40
val eq_refl : constr lazy_t
 
41
 
 
42
val not_ref : constr lazy_t
 
43
val and_typ : constr lazy_t
 
44
 
 
45
val eqdep_ind : constr lazy_t
 
46
val eqdep_rec : constr lazy_t
 
47
 
 
48
val jmeq_ind : unit -> constr
 
49
val jmeq_rec : unit -> constr
 
50
val jmeq_refl : unit -> constr
 
51
 
 
52
val boolind : constr lazy_t
 
53
val sumboolind : constr lazy_t
 
54
val natind : constr lazy_t
 
55
val intind : constr lazy_t
 
56
val existSind : constr lazy_t
 
57
val existS : coq_sigma_data lazy_t
 
58
val prod : coq_sigma_data lazy_t
 
59
 
 
60
val well_founded : constr lazy_t
 
61
val fix : constr lazy_t
 
62
val acc : constr lazy_t
 
63
val acc_inv : constr lazy_t
 
64
val extconstr : constr -> constr_expr
 
65
val extsort : sorts -> constr_expr
 
66
 
 
67
val my_print_constr : env -> constr -> std_ppcmds
 
68
val my_print_constr_expr : constr_expr -> std_ppcmds
 
69
val my_print_evardefs : evar_defs -> std_ppcmds
 
70
val my_print_context : env -> std_ppcmds
 
71
val my_print_rel_context : env -> rel_context -> std_ppcmds
 
72
val my_print_named_context : env -> std_ppcmds
 
73
val my_print_env : env -> std_ppcmds
 
74
val my_print_rawconstr : env -> rawconstr -> std_ppcmds
 
75
val my_print_tycon_type : env -> type_constraint_type -> std_ppcmds
 
76
 
 
77
 
 
78
val debug : int -> std_ppcmds -> unit
 
79
val debug_msg : int -> std_ppcmds -> std_ppcmds
 
80
val trace : std_ppcmds -> unit
 
81
val wf_relations : (constr, constr lazy_t) Hashtbl.t
 
82
 
 
83
type binders = local_binder list
 
84
val app_opt : ('a -> 'a) option -> 'a -> 'a
 
85
val print_args : env -> constr array -> std_ppcmds
 
86
val make_existential : loc -> ?opaque:obligation_definition_status -> 
 
87
  env -> evar_defs ref -> types -> constr
 
88
val make_existential_expr : loc -> 'a -> 'b -> constr_expr
 
89
val string_of_hole_kind : hole_kind -> string
 
90
val evars_of_term : evar_map -> evar_map -> constr -> evar_map
 
91
val non_instanciated_map : env -> evar_defs ref -> evar_map -> evar_map
 
92
val global_kind : logical_kind
 
93
val goal_kind : locality * goal_object_kind
 
94
val global_proof_kind : logical_kind
 
95
val goal_proof_kind : locality * goal_object_kind
 
96
val global_fix_kind : logical_kind
 
97
val goal_fix_kind : locality * goal_object_kind
 
98
 
 
99
val mkSubset : name -> constr -> constr -> constr
 
100
val mkProj1 : constr -> constr -> constr -> constr
 
101
val mkProj1 : constr -> constr -> constr -> constr
 
102
val mk_ex_pi1 : constr -> constr -> constr -> constr
 
103
val mk_ex_pi1 : constr -> constr -> constr -> constr
 
104
val mk_eq : types -> constr -> constr -> types
 
105
val mk_eq_refl : types -> constr -> constr
 
106
val mk_JMeq : types -> constr -> types -> constr -> types
 
107
val mk_JMeq_refl : types -> constr -> constr
 
108
val mk_conj : types list -> types
 
109
val mk_not : types -> types
 
110
 
 
111
val build_dependent_sum : (identifier * types) list -> Proof_type.tactic * types
 
112
val and_tac : (identifier * 'a * constr * Proof_type.tactic) list ->  
 
113
  ((constr -> (identifier * 'a * constr * constr) list) -> Tacexpr.declaration_hook) -> unit
 
114
 
 
115
val destruct_ex : constr -> constr -> constr list
 
116
 
 
117
val id_of_name : name -> identifier
 
118
 
 
119
val definition_message : identifier -> std_ppcmds
 
120
val recursive_message : constant array -> std_ppcmds
 
121
 
 
122
val print_message : std_ppcmds -> unit
 
123
 
 
124
val solve_by_tac : evar_info -> Tacmach.tactic -> constr
 
125
 
 
126
val string_of_list : string -> ('a -> string) -> 'a list -> string
 
127
val string_of_intset : Intset.t -> string
 
128
 
 
129
val pr_evar_defs : evar_defs -> Pp.std_ppcmds
 
130
 
 
131
val tactics_call : string -> Tacexpr.glob_tactic_arg list -> Tacexpr.glob_tactic_expr
 
132
 
 
133
val pp_list : ('a -> Pp.std_ppcmds) -> 'a list -> Pp.std_ppcmds