← Back to branch summary

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

« back to all changes in this revision

Viewing changes to toplevel/command.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:
toplevel/command.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: command.mli 12187 2009-06-13 19:36:59Z msozeau $ i*)
 
10
 
 
11
(*i*)
 
12
open Util
 
13
open Names
 
14
open Term
 
15
open Nametab
 
16
open Declare
 
17
open Library
 
18
open Libnames
 
19
open Nametab
 
20
open Tacexpr
 
21
open Vernacexpr
 
22
open Rawterm
 
23
open Topconstr
 
24
open Decl_kinds
 
25
open Redexpr
 
26
(*i*)
 
27
 
 
28
(*s Declaration functions. The following functions take ASTs,
 
29
   transform them into [constr] and then call the corresponding
 
30
   functions of [Declare]; they return an absolute reference to the
 
31
   defined object *)
 
32
 
 
33
val get_declare_definition_hook : unit -> (Entries.definition_entry -> unit)
 
34
val set_declare_definition_hook : (Entries.definition_entry -> unit) -> unit
 
35
 
 
36
val definition_message : identifier -> unit
 
37
val assumption_message : identifier -> unit
 
38
 
 
39
val declare_definition : identifier -> definition_kind ->
 
40
  local_binder list -> red_expr option -> constr_expr ->
 
41
  constr_expr option -> declaration_hook -> unit
 
42
 
 
43
val syntax_definition : identifier -> identifier list * constr_expr -> 
 
44
  bool -> bool -> unit
 
45
 
 
46
val declare_one_assumption : coercion_flag -> assumption_kind -> Term.types ->
 
47
  Impargs.manual_explicitation list ->
 
48
  bool (* implicit *) -> identifier list (* keep *) -> bool (* inline *) -> Names.variable located  -> unit
 
49
  
 
50
val set_declare_assumption_hook : (types -> unit) -> unit
 
51
 
 
52
val declare_assumption : identifier located list ->
 
53
  coercion_flag -> assumption_kind -> local_binder list -> constr_expr -> 
 
54
  bool -> identifier list -> bool -> unit
 
55
 
 
56
val declare_interning_data : 'a * Constrintern.implicits_env ->
 
57
    string * Topconstr.constr_expr * Topconstr.scope_name option -> unit
 
58
 
 
59
val compute_interning_datas : Environ.env -> Constrintern.var_internalisation_type -> 
 
60
  'a list -> 'b list ->
 
61
  Term.types list ->Impargs.manual_explicitation list list ->
 
62
  'a list *
 
63
    ('b * (Constrintern.var_internalisation_type * Names.identifier list * Impargs.implicits_list *
 
64
              Topconstr.scope_name option list))
 
65
    list
 
66
 
 
67
val check_mutuality : Environ.env -> definition_object_kind ->
 
68
  (identifier * types) list -> unit
 
69
 
 
70
val build_mutual : ((lident * local_binder list * constr_expr option * constructor_expr list) * 
 
71
                                decl_notation) list -> bool -> unit
 
72
 
 
73
val declare_mutual_with_eliminations :
 
74
  bool -> Entries.mutual_inductive_entry -> 
 
75
  (Impargs.manual_explicitation list *
 
76
      Impargs.manual_explicitation list list) list ->
 
77
  mutual_inductive
 
78
 
 
79
type fixpoint_kind =
 
80
  | IsFixpoint of (identifier located option * recursion_order_expr) list
 
81
  | IsCoFixpoint
 
82
 
 
83
type fixpoint_expr = {
 
84
  fix_name : identifier;
 
85
  fix_binders : local_binder list;
 
86
  fix_body : constr_expr;
 
87
  fix_type : constr_expr
 
88
}
 
89
 
 
90
val recursive_message : definition_object_kind ->
 
91
  int array option -> identifier list -> Pp.std_ppcmds
 
92
  
 
93
val declare_fix : bool -> definition_object_kind -> identifier ->
 
94
  constr -> types -> Impargs.manual_explicitation list -> global_reference
 
95
 
 
96
val build_recursive : (Topconstr.fixpoint_expr * decl_notation) list -> bool -> unit
 
97
 
 
98
val build_corecursive : (Topconstr.cofixpoint_expr * decl_notation) list -> bool -> unit
 
99
 
 
100
val build_scheme : (identifier located option * scheme ) list -> unit
 
101
 
 
102
val build_combined_scheme : identifier located -> identifier located list -> unit
 
103
 
 
104
val generalize_constr_expr : constr_expr -> local_binder list -> constr_expr
 
105
 
 
106
val abstract_constr_expr : constr_expr -> local_binder list -> constr_expr
 
107
 
 
108
(* A hook start_proof calls on the type of the definition being started *)
 
109
val set_start_hook : (types -> unit) -> unit
 
110
 
 
111
val start_proof : identifier -> goal_kind -> types ->
 
112
  ?init_tac:Proof_type.tactic -> ?compute_guard:bool -> declaration_hook -> unit
 
113
 
 
114
val start_proof_com : goal_kind -> 
 
115
  (lident option * (local_binder list * constr_expr)) list ->
 
116
  declaration_hook -> unit
 
117
 
 
118
(* A hook the next three functions pass to cook_proof *)
 
119
val set_save_hook : (Refiner.pftreestate -> unit) -> unit
 
120
 
 
121
(*s [save_named b] saves the current completed proof under the name it
 
122
was started; boolean [b] tells if the theorem is declared opaque; it
 
123
fails if the proof is not completed *)
 
124
 
 
125
val save_named : bool -> unit
 
126
 
 
127
(* [save_anonymous b name] behaves as [save_named] but declares the theorem
 
128
under the name [name] and respects the strength of the declaration *)
 
129
 
 
130
val save_anonymous : bool -> identifier -> unit
 
131
 
 
132
(* [save_anonymous_with_strength s b name] behaves as [save_anonymous] but
 
133
   declares the theorem under the name [name] and gives it the
 
134
   strength [strength] *)
 
135
 
 
136
val save_anonymous_with_strength : theorem_kind -> bool -> identifier -> unit
 
137
 
 
138
(* [admit ()] aborts the current goal and save it as an assmumption *)
 
139
 
 
140
val admit : unit -> unit
 
141
 
 
142
(* [get_current_context ()] returns the evar context and env of the
 
143
   current open proof if any, otherwise returns the empty evar context
 
144
   and the current global env *)
 
145
 
 
146
val get_current_context : unit -> Evd.evar_map * Environ.env
 
147
 
 
148