← Back to branch summary

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

« back to all changes in this revision

Viewing changes to proofs/tacmach.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:
proofs/tacmach.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: tacmach.mli 12168 2009-06-06 21:34:37Z herbelin $ i*)
 
10
 
 
11
(*i*)
 
12
open Names
 
13
open Term
 
14
open Sign
 
15
open Environ
 
16
open Evd
 
17
open Reduction
 
18
open Proof_trees
 
19
open Proof_type
 
20
open Refiner
 
21
open Redexpr
 
22
open Tacexpr
 
23
open Rawterm
 
24
(*i*)
 
25
 
 
26
(* Operations for handling terms under a local typing context. *)
 
27
 
 
28
type 'a sigma   = 'a Evd.sigma;;
 
29
type validation = Proof_type.validation;;
 
30
type tactic     = Proof_type.tactic;;
 
31
 
 
32
val sig_it  : 'a sigma   -> 'a
 
33
val project : goal sigma -> evar_map
 
34
 
 
35
val re_sig : 'a -> evar_map -> 'a sigma
 
36
 
 
37
val unpackage : 'a sigma -> evar_map ref * 'a
 
38
val repackage : evar_map ref -> 'a -> 'a sigma
 
39
val apply_sig_tac :
 
40
  evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
 
41
 
 
42
val pf_concl              : goal sigma -> types
 
43
val pf_env                : goal sigma -> env
 
44
val pf_hyps               : goal sigma -> named_context
 
45
(*i val pf_untyped_hyps       : goal sigma -> (identifier * constr) list i*)
 
46
val pf_hyps_types         : goal sigma -> (identifier * types) list
 
47
val pf_nth_hyp_id         : goal sigma -> int -> identifier
 
48
val pf_last_hyp           : goal sigma -> named_declaration
 
49
val pf_ids_of_hyps        : goal sigma -> identifier list
 
50
val pf_global             : goal sigma -> identifier -> constr
 
51
val pf_parse_const        : goal sigma -> string -> constr
 
52
val pf_type_of            : goal sigma -> constr -> types
 
53
val pf_check_type         : goal sigma -> constr -> types -> unit
 
54
val hnf_type_of           : goal sigma -> constr -> types
 
55
 
 
56
val pf_interp_constr      : goal sigma -> Topconstr.constr_expr -> constr
 
57
val pf_interp_type        : goal sigma -> Topconstr.constr_expr -> types
 
58
 
 
59
val pf_get_hyp            : goal sigma -> identifier -> named_declaration
 
60
val pf_get_hyp_typ        : goal sigma -> identifier -> types
 
61
 
 
62
val pf_get_new_id  : identifier      -> goal sigma -> identifier
 
63
val pf_get_new_ids : identifier list -> goal sigma -> identifier list
 
64
 
 
65
val pf_reduction_of_red_expr : goal sigma -> red_expr -> constr -> constr
 
66
 
 
67
 
 
68
val pf_apply : (env -> evar_map -> 'a) -> goal sigma -> 'a
 
69
val pf_reduce : 
 
70
  (env -> evar_map -> constr -> constr) ->
 
71
    goal sigma -> constr -> constr
 
72
 
 
73
val pf_whd_betadeltaiota       : goal sigma -> constr -> constr
 
74
val pf_whd_betadeltaiota_stack : goal sigma -> constr -> constr * constr list 
 
75
val pf_hnf_constr              : goal sigma -> constr -> constr
 
76
val pf_red_product             : goal sigma -> constr -> constr
 
77
val pf_nf                      : goal sigma -> constr -> constr
 
78
val pf_nf_betaiota             : goal sigma -> constr -> constr
 
79
val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
 
80
val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
 
81
val pf_compute                 : goal sigma -> constr -> constr
 
82
val pf_unfoldn    : (Termops.occurrences * evaluable_global_reference) list
 
83
        -> goal sigma -> constr -> constr
 
84
 
 
85
val pf_const_value : goal sigma -> constant -> constr
 
86
val pf_conv_x      : goal sigma -> constr -> constr -> bool
 
87
val pf_conv_x_leq  : goal sigma -> constr -> constr -> bool
 
88
 
 
89
type transformation_tactic = proof_tree -> (goal list * validation)
 
90
 
 
91
val frontier : transformation_tactic
 
92
 
 
93
 
 
94
(*s Functions for handling the state of the proof editor. *)
 
95
 
 
96
type pftreestate = Refiner.pftreestate
 
97
 
 
98
val proof_of_pftreestate    : pftreestate -> proof_tree
 
99
val cursor_of_pftreestate   : pftreestate -> int list
 
100
val is_top_pftreestate      : pftreestate -> bool
 
101
val evc_of_pftreestate      : pftreestate -> evar_map
 
102
val top_goal_of_pftreestate : pftreestate -> goal sigma
 
103
val nth_goal_of_pftreestate : int -> pftreestate -> goal sigma
 
104
val traverse                : int -> pftreestate -> pftreestate
 
105
val weak_undo_pftreestate   : pftreestate -> pftreestate
 
106
val solve_nth_pftreestate   : int -> tactic -> pftreestate -> pftreestate
 
107
val solve_pftreestate       : tactic -> pftreestate -> pftreestate
 
108
val mk_pftreestate          : goal -> pftreestate
 
109
val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
 
110
val extract_pftreestate     : pftreestate -> constr
 
111
val first_unproven          : pftreestate -> pftreestate
 
112
val last_unproven           : pftreestate -> pftreestate
 
113
val nth_unproven            : int -> pftreestate -> pftreestate
 
114
val node_prev_unproven      : int -> pftreestate -> pftreestate
 
115
val node_next_unproven      : int -> pftreestate -> pftreestate
 
116
val next_unproven           : pftreestate -> pftreestate
 
117
val prev_unproven           : pftreestate -> pftreestate
 
118
val top_of_tree             : pftreestate -> pftreestate
 
119
val change_constraints_pftreestate :
 
120
  evar_map -> pftreestate -> pftreestate
 
121
 
 
122
(*s The most primitive tactics. *)
 
123
 
 
124
val refiner                   : rule -> tactic
 
125
val introduction_no_check     : identifier -> tactic
 
126
val internal_cut_no_check     : bool -> identifier -> types -> tactic
 
127
val internal_cut_rev_no_check : bool -> identifier -> types -> tactic
 
128
val refine_no_check           : constr -> tactic
 
129
val convert_concl_no_check    : types -> cast_kind -> tactic
 
130
val convert_hyp_no_check      : named_declaration -> tactic
 
131
val thin_no_check             : identifier list -> tactic
 
132
val thin_body_no_check        : identifier list -> tactic
 
133
val move_hyp_no_check         :
 
134
  bool -> identifier -> identifier move_location -> tactic
 
135
val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 
136
val order_hyps : identifier list -> tactic
 
137
val mutual_fix      :
 
138
  identifier -> int -> (identifier * int * constr) list -> tactic
 
139
val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
 
140
val mutual_fix_with_index :
 
141
  identifier -> int -> (identifier * int * constr) list -> int -> tactic
 
142
val mutual_cofix_with_index : 
 
143
  identifier -> (identifier * constr) list -> int -> tactic
 
144
 
 
145
(*s The most primitive tactics with consistency and type checking *)
 
146
 
 
147
val introduction     : identifier -> tactic
 
148
val internal_cut     : bool -> identifier -> types -> tactic
 
149
val internal_cut_rev : bool -> identifier -> types -> tactic
 
150
val refine           : constr -> tactic
 
151
val convert_concl    : types -> cast_kind -> tactic
 
152
val convert_hyp      : named_declaration -> tactic
 
153
val thin             : identifier list -> tactic
 
154
val thin_body        : identifier list -> tactic
 
155
val move_hyp         : bool -> identifier -> identifier move_location -> tactic
 
156
val rename_hyp       : (identifier*identifier) list -> tactic
 
157
 
 
158
(*s Tactics handling a list of goals. *)
 
159
 
 
160
type validation_list = proof_tree list -> proof_tree list
 
161
 
 
162
type tactic_list = (goal list sigma) -> (goal list sigma) * validation_list
 
163
 
 
164
val first_goal         : 'a list sigma -> 'a sigma
 
165
val goal_goal_list     : 'a sigma -> 'a list sigma
 
166
val apply_tac_list     : tactic -> tactic_list
 
167
val then_tactic_list   : tactic_list -> tactic_list -> tactic_list
 
168
val tactic_list_tactic : tactic_list -> tactic
 
169
val tclFIRSTLIST       : tactic_list list -> tactic_list
 
170
val tclIDTAC_list      : tactic_list
 
171
 
 
172
(*s Pretty-printing functions (debug only). *)
 
173
val pr_gls    : goal sigma -> Pp.std_ppcmds
 
174
val pr_glls   : goal list sigma -> Pp.std_ppcmds