blob: 8b123eb7b0e37d9868d0e275ab8e52bd963f1ccd (
plain)
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
|
DECLARE PLUGIN "tuto3_plugin"
open Ltac_plugin
open Construction_game
(* This one is necessary, to avoid message about missing wit_string *)
open Stdarg
VERNAC COMMAND EXTEND ShowTypeConstruction CLASSIFIED AS QUERY
| [ "Tuto3_1" ] ->
[ let env = Global.env () in
let evd = Evd.from_env env in
let evd, s = Evd.new_sort_variable Evd.univ_rigid evd in
let new_type_2 = EConstr.mkSort s in
let evd, _ =
Typing.type_of (Global.env()) (Evd.from_env (Global.env())) new_type_2 in
Feedback.msg_notice
(Termops.print_constr_env env evd new_type_2) ]
END
VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY
| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ]
END
TACTIC EXTEND collapse_hyps
| [ "pack" "hypothesis" ident(i) ] ->
[ Tuto_tactic.pack_tactic i ]
END
(* More advanced examples, where automatic proof happens but
no tactic is being called explicitely. The first one uses
type classes. *)
VERNAC COMMAND EXTEND TriggerClasses CLASSIFIED AS QUERY
| [ "Tuto3_3" int(n) ] -> [ example_classes n ]
END
(* The second one uses canonical structures. *)
VERNAC COMMAND EXTEND TriggerCanonical CLASSIFIED AS QUERY
| [ "Tuto3_4" int(n) ] -> [ example_canonical n ]
END
|
