← Back to branch summary

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

« back to all changes in this revision

Viewing changes to dev/base_include

  • 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:
dev/base_include
 
1
 
 
2
(* File to include to get some Coq facilities under the ocaml toplevel.
 
3
   This file is loaded by include *)
 
4
 
 
5
#cd".";;
 
6
#directory "parsing";;
 
7
#directory "interp";;
 
8
#directory "toplevel";;
 
9
#directory "library";;
 
10
#directory "kernel";;
 
11
#directory "pretyping";;
 
12
#directory "lib";;
 
13
#directory "proofs";;
 
14
#directory "tactics";;
 
15
#directory "translate";;
 
16
 
 
17
#directory "+camlp4";; (* lazy solution: add both of camlp4/5 so that *)
 
18
#directory "+camlp5";; (* Gramext is found in top_printers.ml *)
 
19
 
 
20
#use "top_printers.ml";;
 
21
#use "vm_printers.ml";;
 
22
 
 
23
#install_printer  (* identifier *) ppid;;
 
24
#install_printer  (* identifier *) ppidset;;
 
25
#install_printer  (* Intset.t *) ppintset;;
 
26
#install_printer  (* label *) pplab;;
 
27
#install_printer  (* mod_self_id *) ppmsid;;
 
28
#install_printer  (* mod_bound_id *) ppmbid;;
 
29
#install_printer  (* dir_path *) ppdir;;
 
30
#install_printer  (* module_path *) ppmp;;
 
31
#install_printer  (* section_path *)  ppsp;;
 
32
#install_printer  (* qualid *)  ppqualid;;
 
33
#install_printer  (* kernel_name *) ppkn;;
 
34
#install_printer  (* constant *) ppcon;;
 
35
#install_printer  (* cl_index *) ppclindex;;
 
36
#install_printer  (* constr *)  print_pure_constr;; 
 
37
#install_printer  (* patch *) ppripos;;
 
38
#install_printer  (* values *) ppvalues;;
 
39
#install_printer  (* Idpred.t *) pp_idpred;;
 
40
#install_printer  (* Cpred.t *) pp_cpred;;
 
41
#install_printer  (* transparent_state *) pp_transparent_state;;
 
42
#install_printer ppzipper;;
 
43
#install_printer ppstack;;
 
44
#install_printer ppatom;;
 
45
#install_printer ppwhd;;
 
46
#install_printer ppvblock;;
 
47
#install_printer  (* bigint *) ppbigint;;
 
48
#install_printer  (* loc *) pploc;;
 
49
#install_printer  (* substitution *) prsubst;;
 
50
 
 
51
(* Open main files *)
 
52
 
 
53
open Names
 
54
open Term
 
55
open Typeops
 
56
open Univ
 
57
open Inductive
 
58
open Indtypes
 
59
open Cooking
 
60
open Closure
 
61
open Reduction
 
62
open Safe_typing
 
63
open Declare
 
64
open Declaremods
 
65
open Impargs
 
66
open Libnames
 
67
open Nametab
 
68
open Library
 
69
 
 
70
open Cases
 
71
open Pattern
 
72
open Cbv
 
73
open Classops
 
74
open Pretyping
 
75
open Pretyping.Default
 
76
open Pretyping.Default.Cases
 
77
open Cbv
 
78
open Classops
 
79
open Clenv
 
80
open Rawterm
 
81
open Coercion
 
82
open Coercion.Default
 
83
open Recordops
 
84
open Detyping
 
85
open Reductionops
 
86
open Evarconv
 
87
open Retyping
 
88
open Evarutil
 
89
open Tacred
 
90
open Evd
 
91
open Termops
 
92
open Indrec
 
93
open Typing
 
94
open Inductiveops
 
95
open Unification
 
96
open Matching
 
97
 
 
98
open Constrextern
 
99
open Constrintern
 
100
open Coqlib
 
101
open Genarg
 
102
open Modintern
 
103
open Notation
 
104
open Ppextend
 
105
open Reserve
 
106
open Syntax_def
 
107
open Topconstr
 
108
 
 
109
open Clenvtac
 
110
open Evar_refiner
 
111
open Logic
 
112
open Pfedit
 
113
open Proof_trees
 
114
open Proof_type
 
115
open Redexpr
 
116
open Refiner
 
117
open Tacmach
 
118
open Decl_proof_instr
 
119
open Tactic_debug
 
120
open Decl_mode
 
121
 
 
122
open Auto
 
123
open Autorewrite
 
124
open Contradiction
 
125
open Dhyp
 
126
open Eauto
 
127
open Elim
 
128
open Equality
 
129
open Evar_tactics
 
130
open Extraargs
 
131
open Extratactics
 
132
open Hiddentac
 
133
open Hipattern
 
134
open Inv
 
135
open Leminv
 
136
open Refine
 
137
open Tacinterp
 
138
open Tacticals
 
139
open Tactics
 
140
 
 
141
open Cerrors
 
142
open Class
 
143
open Command
 
144
open Coqinit
 
145
open Coqtop
 
146
open Discharge
 
147
open Himsg
 
148
open Metasyntax
 
149
open Mltop
 
150
open Record
 
151
open Toplevel
 
152
open Vernacentries
 
153
open Vernacinterp
 
154
open Vernac
 
155
 
 
156
(* Various utilities *)
 
157
 
 
158
let qid = Libnames.qualid_of_string;;
 
159
 
 
160
(* parsing of terms *)
 
161
 
 
162
let parse_constr = Pcoq.parse_string Pcoq.Constr.constr;;
 
163
let parse_tac    = Pcoq.parse_string Pcoq.Tactic.tactic;;
 
164
let parse_vernac = Pcoq.parse_string Pcoq.Vernac_.vernac;;
 
165
 
 
166
(* build a term of type rawconstr without type-checking or resolution of 
 
167
   implicit syntax *)
 
168
 
 
169
let e s =
 
170
  Constrintern.intern_constr Evd.empty (Global.env()) (parse_constr s);;
 
171
 
 
172
(* build a term of type constr with type-checking and resolution of 
 
173
   implicit syntax *)
 
174
 
 
175
let constr_of_string s = 
 
176
  Constrintern.interp_constr Evd.empty (Global.env()) (parse_constr s);;
 
177
 
 
178
(* get the body of a constant *)
 
179
 
 
180
open Declarations;;
 
181
 
 
182
let constbody_of_string s =
 
183
  let b = Global.lookup_constant (Nametab.locate_constant (qualid_of_sp (path_of_string s))) in
 
184
  Option.get b.const_body;;
 
185
 
 
186
(* Get the current goal *)
 
187
 
 
188
let getgoal x = top_goal_of_pftreestate (Pfedit.get_pftreestate x);;
 
189
 
 
190
let get_nth_goal n = nth_goal_of_pftreestate n (Pfedit.get_pftreestate ());;
 
191
let current_goal () = get_nth_goal 1;;
 
192
 
 
193
let pf_e gl s = 
 
194
  Constrintern.interp_constr (project gl) (pf_env gl) (parse_constr s);;
 
195
 
 
196
open Toplevel
 
197
let go = loop
 
198