-
Notifications
You must be signed in to change notification settings - Fork 0
/
_CoqProject
51 lines (49 loc) · 855 Bytes
/
_CoqProject
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
-R theories/ Ltac2
-I src/
src/tac2dyn.ml
src/tac2dyn.mli
src/tac2expr.mli
src/tac2types.mli
src/tac2env.ml
src/tac2env.mli
src/tac2print.ml
src/tac2print.mli
src/tac2intern.ml
src/tac2intern.mli
src/tac2interp.ml
src/tac2interp.mli
src/tac2entries.ml
src/tac2entries.mli
src/tac2ffi.ml
src/tac2ffi.mli
src/tac2qexpr.mli
src/tac2quote.ml
src/tac2quote.mli
src/tac2match.ml
src/tac2match.mli
src/tac2core.ml
src/tac2core.mli
src/tac2extffi.ml
src/tac2extffi.mli
src/tac2tactics.ml
src/tac2tactics.mli
src/tac2stdlib.ml
src/tac2stdlib.mli
src/g_ltac2.mlg
src/ltac2_plugin.mlpack
theories/Init.v
theories/Int.v
theories/Char.v
theories/String.v
theories/Ident.v
theories/Array.v
theories/Control.v
theories/Message.v
theories/Constr.v
theories/Pattern.v
theories/Fresh.v
theories/Std.v
theories/Env.v
theories/Notations.v
theories/Ltac1.v
theories/Ltac2.v