← Back to branch summary

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

« back to all changes in this revision

Viewing changes to ide/coq_commands.ml

  • 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:
ide/coq_commands.ml
 
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
(* $Id: coq_commands.ml 10994 2008-05-26 16:21:31Z jnarboux $ *)
 
10
 
 
11
let commands = [
 
12
  [(* "Abort"; *)
 
13
   "Add Abstract Ring A Aplus Amult Aone Azero Ainv Aeq T.";
 
14
   "Add Abstract Semi Ring A Aplus Amult Aone Azero Aeq T.";
 
15
   "Add Field";
 
16
   "Add LoadPath";
 
17
   "Add ML Path";
 
18
   "Add Morphism";
 
19
   "Add Printing If";
 
20
   "Add Printing Let";
 
21
   "Add Rec LoadPath";
 
22
   "Add Rec ML Path";
 
23
   "Add Ring A Aplus Amult Aone Azero Ainv Aeq T [ c1 ... cn ]. ";
 
24
   "Add Semi Ring A Aplus Amult Aone Azero Aeq T [ c1 ... cn ].";
 
25
   "Add Relation";
 
26
   "Add Setoid";
 
27
   "Axiom";];
 
28
  [(* "Back"; *) ];
 
29
  ["Canonical Structure";
 
30
   "Chapter";
 
31
   "Coercion";
 
32
   "Coercion Local";
 
33
   "CoFixpoint";
 
34
   "CoInductive";
 
35
  ];
 
36
  ["Declare ML Module";
 
37
   "Defined.";
 
38
   "Definition";
 
39
   "Derive Dependent Inversion";
 
40
   "Derive Dependent Inversion__clear";
 
41
   "Derive Inversion";
 
42
   "Derive Inversion__clear";
 
43
  ];
 
44
  ["End";
 
45
   "End Silent.";
 
46
   "Eval"; 
 
47
   "Extract Constant";
 
48
   "Extract Inductive";
 
49
   "Extraction Inline";
 
50
   "Extraction Language";
 
51
   "Extraction NoInline";];
 
52
  ["Fact";
 
53
   "Fixpoint";
 
54
   "Focus";];
 
55
  ["Global Variable";
 
56
   "Goal";
 
57
   "Grammar";];
 
58
  ["Hint";
 
59
   "Hint Constructors";
 
60
   "Hint Extern";
 
61
   "Hint Immediate";
 
62
   "Hint Resolve";
 
63
   "Hint Rewrite";
 
64
   "Hint Unfold";
 
65
   "Hypothesis";];
 
66
  ["Identity Coercion";
 
67
   "Implicit Arguments";
 
68
   "Inductive";
 
69
   "Infix";
 
70
   ];
 
71
  ["Lemma";
 
72
   "Load";
 
73
   "Load Verbose";
 
74
   "Local";
 
75
   "Ltac";
 
76
  ];
 
77
  ["Module";
 
78
   "Module Type";
 
79
   "Mutual Inductive";];
 
80
  ["Notation";
 
81
   "Next Obligation";];
 
82
  ["Opaque";
 
83
   "Obligations Tactic";];
 
84
  ["Parameter";
 
85
   "Proof.";
 
86
   "Program Definition";
 
87
   "Program Fixpoint";     
 
88
   "Program Lemma";
 
89
   "Program Theorem";
 
90
  ];
 
91
  ["Qed.";
 
92
   ];
 
93
  ["Read Module";
 
94
   "Record";
 
95
   "Remark";
 
96
   "Remove LoadPath";
 
97
   "Remove Printing If";
 
98
   "Remove Printing Let";
 
99
   "Require";
 
100
   "Require Export";
 
101
   "Require Import";
 
102
   "Reset Extraction Inline";
 
103
   "Restore State"; 
 
104
   ];
 
105
  [  "Save.";
 
106
     "Scheme";
 
107
     "Section";
 
108
     "Set Extraction AutoInline";
 
109
     "Set Extraction Optimize";
 
110
     "Set Hyps__limit";
 
111
     "Set Implicit Arguments";
 
112
     (*"Set Printing Coercion";
 
113
     "Set Printing Coercions";
 
114
     "Set Printing Synth";*)
 
115
     "Set Printing Wildcard";
 
116
     "Set Silent.";
 
117
     "Set Undo";
 
118
     (*"Show";
 
119
     "Show Conjectures";
 
120
     "Show Implicits";
 
121
     "Show Intro";
 
122
     "Show Intros";
 
123
     "Show Programs";
 
124
     "Show Proof";
 
125
     "Show Script";
 
126
     "Show Tree";*)
 
127
     "Structure";
 
128
     (* "Suspend"; *)
 
129
     "Syntactic Definition";
 
130
     "Syntax";];
 
131
  [
 
132
   "Test Printing If";
 
133
   "Test Printing Let";
 
134
   "Test Printing Synth";
 
135
   "Test Printing Wildcard";
 
136
   "Theorem";
 
137
   "Time";
 
138
   "Transparent";];
 
139
  [(* "Undo"; *)
 
140
   "Unfocus";
 
141
   "Unset Extraction AutoInline";
 
142
   "Unset Extraction Optimize";
 
143
   "Unset Hyps__limit";
 
144
   "Unset Implicit Arguments";
 
145
   (*
 
146
   "Unset Printing Coercion";
 
147
   "Unset Printing Coercions";
 
148
   "Unset Printing Synth"; *)
 
149
   "Unset Printing Wildcard";
 
150
   "Unset Silent.";
 
151
   "Unset Undo";];
 
152
  ["Variable";
 
153
   "Variables";];
 
154
  ["Write State";];
 
155
]
 
156
 
 
157
let state_preserving = [
 
158
  "Check";
 
159
  "Eval";
 
160
  "Eval lazy in";
 
161
  "Eval vm_compute in";
 
162
  "Eval compute in";
 
163
  "Extraction";
 
164
  "Extraction Library";
 
165
  "Extraction Module";
 
166
  "Inspect";
 
167
  "Locate";
 
168
  
 
169
  "Obligations";
 
170
  "Print";
 
171
  "Print All.";
 
172
  "Print Classes";
 
173
  "Print Coercion Paths";
 
174
  "Print Coercions";
 
175
  "Print Extraction Inline";
 
176
  "Print Grammar";
 
177
  "Print Graph";
 
178
  "Print Hint";
 
179
  "Print Hint *";
 
180
  "Print HintDb";
 
181
  "Print Implicit";
 
182
  "Print LoadPath";
 
183
  "Print ML Modules";
 
184
  "Print ML Path";
 
185
  "Print Module";
 
186
  "Print Module Type";
 
187
  "Print Modules";
 
188
  "Print Proof";
 
189
  "Print Rewrite HintDb";
 
190
  "Print Setoids";
 
191
  "Print Scope";
 
192
  "Print Scopes.";
 
193
  "Print Section";
 
194
  
 
195
  "Print Table Printing If.";
 
196
  "Print Table Printing Let.";
 
197
  "Print Tables.";
 
198
  "Print Term";
 
199
 
 
200
  "Print Visibility";
 
201
 
 
202
  "Pwd.";
 
203
 
 
204
  "Recursive Extraction";
 
205
  "Recursive Extraction Library";
 
206
 
 
207
  "Search";
 
208
  "SearchAbout";
 
209
  "SearchPattern";
 
210
  "SearchRewrite";
 
211
 
 
212
  "Show";
 
213
  "Show Conjectures";
 
214
  "Show Existentials";
 
215
  "Show Implicits";
 
216
  "Show Intro";
 
217
  "Show Intros";
 
218
  "Show Proof";
 
219
  "Show Script";
 
220
  "Show Tree";
 
221
 
 
222
  "Test Printing If";
 
223
  "Test Printing Let";
 
224
  "Test Printing Synth";
 
225
  "Test Printing Wildcard";
 
226
 
 
227
  "Whelp Hint";
 
228
  "Whelp Locate";
 
229
]
 
230
 
 
231
 
 
232
let tactics = 
 
233
  [
 
234
    [
 
235
      "abstract";
 
236
      "absurd";
 
237
      "apply";
 
238
      "apply __ with";
 
239
      "assert";
 
240
      "assert (__:__)";
 
241
      "assert (__:=__)";
 
242
      "assumption";
 
243
      "auto";
 
244
      "auto with";
 
245
      "autorewrite";
 
246
    ];
 
247
 
 
248
   [
 
249
     "case";
 
250
     "case __ with";
 
251
     "casetype";
 
252
     "cbv";
 
253
     "cbv in";
 
254
     "change";
 
255
     "change __ in";
 
256
     "clear";
 
257
     "clearbody";
 
258
     "cofix";
 
259
     "compare";
 
260
     "compute";
 
261
     "compute in";
 
262
     "congruence";
 
263
     "constructor";
 
264
     "constructor __ with";
 
265
     "contradiction";
 
266
     "cut";
 
267
     "cutrewrite";
 
268
   ];
 
269
 
 
270
   [
 
271
     "decide equality";
 
272
     "decompose";
 
273
     "decompose record";
 
274
     "decompose sum";
 
275
     "dependent inversion";
 
276
     "dependent inversion __ with";
 
277
     "dependent inversion__clear";
 
278
     "dependent inversion__clear __ with";
 
279
     "dependent rewrite ->";
 
280
     "dependent rewrite <-";
 
281
     "destruct";
 
282
     "discriminate";
 
283
     "do";
 
284
     "double induction";
 
285
   ];
 
286
 
 
287
   [
 
288
     "eapply";
 
289
     "eauto";
 
290
     "eauto with";
 
291
     "eexact";
 
292
     "elim";
 
293
     "elim __ using";
 
294
     "elim __ with";
 
295
     "elimtype";
 
296
     "exact";
 
297
     "exists";
 
298
   ];
 
299
 
 
300
   [
 
301
     "fail";
 
302
     "field";
 
303
     "first";
 
304
     "firstorder";
 
305
     "firstorder using";
 
306
     "firstorder with";
 
307
     "fix";
 
308
     "fix __ with";
 
309
     "fold";
 
310
     "fold __ in";
 
311
     "fourier";
 
312
     "functional induction";
 
313
   ];
 
314
 
 
315
   [
 
316
     "generalize";
 
317
     "generalize dependent";
 
318
   ];
 
319
   
 
320
   [
 
321
     "hnf";
 
322
   ];
 
323
 
 
324
   [
 
325
     "idtac";
 
326
     "induction";
 
327
     "info";
 
328
     "injection";
 
329
     "instantiate (__:=__)";
 
330
     "intro";
 
331
     "intro after";
 
332
     "intro __ after";
 
333
     "intros";
 
334
     "intros until";
 
335
     "intuition";
 
336
     "inversion";
 
337
     "inversion __ in";
 
338
     "inversion __ using";
 
339
     "inversion __ using __ in";
 
340
     "inversion__clear";
 
341
     "inversion__clear __ in";
 
342
   ];
 
343
 
 
344
   [
 
345
     "jp <n>";
 
346
     "jp";
 
347
   ];
 
348
 
 
349
   [
 
350
     "lapply";
 
351
     "lazy";
 
352
     "lazy in";
 
353
     "left";
 
354
   ];
 
355
 
 
356
   [
 
357
     "move __ after";
 
358
   ];
 
359
 
 
360
   [
 
361
     "omega";
 
362
   ];
 
363
 
 
364
   [
 
365
     "pattern";
 
366
     "pose";
 
367
     "pose __:=__)";
 
368
     "progress";
 
369
   ];
 
370
 
 
371
   [
 
372
     "quote";
 
373
   ];
 
374
 
 
375
   [
 
376
     "red";
 
377
     "red in";
 
378
     "refine";
 
379
     "reflexivity";
 
380
     "rename __ into";
 
381
     "repeat";
 
382
     "replace __ with";
 
383
     "rewrite";
 
384
     "rewrite __ in";
 
385
     "rewrite <-";
 
386
     "rewrite <- __ in";
 
387
     "right";
 
388
     "ring";
 
389
   ];
 
390
 
 
391
   [
 
392
     "set";
 
393
     "set (__:=__)";
 
394
     "setoid__replace";
 
395
     "setoid__rewrite";
 
396
     "simpl";
 
397
     "simpl __ in";
 
398
     "simple destruct";
 
399
     "simple induction";
 
400
     "simple inversion";
 
401
     "simplify__eq";
 
402
     "solve";
 
403
     "split";
 
404
(*     "split__Rabs";
 
405
     "split__Rmult";
 
406
*)
 
407
     "subst";
 
408
     "symmetry";
 
409
     "symmetry in";
 
410
   ];
 
411
 
 
412
   [
 
413
     "tauto";
 
414
     "transitivity";
 
415
     "trivial";
 
416
     "try";
 
417
   ];
 
418
   
 
419
   [
 
420
     "unfold";
 
421
     "unfold __ in";
 
422
   ];
 
423
]
 
424
 
 
425