diff options
| author | Pierre-Marie Pédrot | 2018-10-31 17:57:47 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-11-05 18:36:00 +0100 |
| commit | 0fe2b5d4d63bcbc63d48a386949094c23e4c274e (patch) | |
| tree | f9e8bcbf17bca3853f088932d56a24588b2b13f7 /tuto3 | |
| parent | 6617535fd1666a7010c6eb9a81b4405e9d4f9c8d (diff) | |
Port to coqpp.
Diffstat (limited to 'tuto3')
| -rw-r--r-- | tuto3/_CoqProject | 4 | ||||
| -rw-r--r-- | tuto3/src/g_tuto3.mlg (renamed from tuto3/src/g_tuto3.ml4) | 16 |
2 files changed, 12 insertions, 8 deletions
diff --git a/tuto3/_CoqProject b/tuto3/_CoqProject index 6a3c1978a7..e2a60a430f 100644 --- a/tuto3/_CoqProject +++ b/tuto3/_CoqProject @@ -8,5 +8,5 @@ src/tuto_tactic.ml src/tuto_tactic.mli src/construction_game.ml src/construction_game.mli -src/g_tuto3.ml4 -src/tuto3_plugin.mlpack
\ No newline at end of file +src/g_tuto3.mlg +src/tuto3_plugin.mlpack diff --git a/tuto3/src/g_tuto3.ml4 b/tuto3/src/g_tuto3.mlg index 71c6be16c8..82ba45726e 100644 --- a/tuto3/src/g_tuto3.ml4 +++ b/tuto3/src/g_tuto3.mlg @@ -1,5 +1,7 @@ DECLARE PLUGIN "tuto3_plugin" +{ + open Ltac_plugin open Construction_game @@ -7,36 +9,38 @@ 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 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 - (Printer.pr_econstr_env env evd new_type_2) ] + (Printer.pr_econstr_env env evd new_type_2) } END VERNAC COMMAND EXTEND ShowOneConstruction CLASSIFIED AS QUERY -| [ "Tuto3_2" ] -> [ example_sort_app_lambda () ] +| [ "Tuto3_2" ] -> { example_sort_app_lambda () } END TACTIC EXTEND collapse_hyps | [ "pack" "hypothesis" ident(i) ] -> - [ Tuto_tactic.pack_tactic 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 ] +| [ "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 ] +| [ "Tuto3_4" int(n) ] -> { example_canonical n } END |