diff options
| author | Yves Bertot | 2018-05-02 14:18:39 +0200 |
|---|---|---|
| committer | Yves Bertot | 2018-05-02 14:18:39 +0200 |
| commit | f893ebe4189bb2ecb085e6e139e13c9dadd4611a (patch) | |
| tree | 921478737eeb57c18114c3e9c8e8e3cf0cb2bd70 | |
| parent | 3df17ed7972dc404cc8519ae9bfd42f75e278e0b (diff) | |
first examples of commands taking arguments
| -rw-r--r-- | tuto1/Makefile | 14 | ||||
| -rw-r--r-- | tuto1/_CoqProject | 5 | ||||
| -rw-r--r-- | tuto1/src/g_tuto1.ml4 | 24 | ||||
| -rw-r--r-- | tuto1/src/tuto1_plugin.mlpack | 1 |
4 files changed, 44 insertions, 0 deletions
diff --git a/tuto1/Makefile b/tuto1/Makefile new file mode 100644 index 0000000000..e0e197650d --- /dev/null +++ b/tuto1/Makefile @@ -0,0 +1,14 @@ +ifeq "$(COQBIN)" "" + COQBIN=$(dir $(shell which coqtop))/ +endif + +%: Makefile.coq + +Makefile.coq: _CoqProject + $(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq + +tests: all + @$(MAKE) -C tests -s clean + @$(MAKE) -C tests -s all + +-include Makefile.coq diff --git a/tuto1/_CoqProject b/tuto1/_CoqProject new file mode 100644 index 0000000000..7a191a961d --- /dev/null +++ b/tuto1/_CoqProject @@ -0,0 +1,5 @@ +-R theories/ Tuto0 +-I src + +src/g_tuto1.ml4 +src/tuto1_plugin.mlpack
\ No newline at end of file diff --git a/tuto1/src/g_tuto1.ml4 b/tuto1/src/g_tuto1.ml4 new file mode 100644 index 0000000000..6ff97ae5cf --- /dev/null +++ b/tuto1/src/g_tuto1.ml4 @@ -0,0 +1,24 @@ +open Pp +(* This one is necessary, to avoid message about missing wit_string *) +open Stdarg + +VERNAC COMMAND EXTEND HelloWorld CLASSIFIED AS QUERY +| [ "Hello" string(s)] -> + [ Feedback.msg_notice (strbrk "Hello " ++ str s) ] +END + +(* reference is allowed as a syntactic entry, but so are all the entries + found the signature of module Prim in file coq/parsing/pcoq.mli *) + +VERNAC COMMAND EXTEND HelloAgain CLASSIFIED AS QUERY +| [ "HelloAgain" reference(r)] -> +(* The function Libnames.pr_reference was found by searchin all mli files + for a function of type reference -> Pp.t *) + [ Feedback.msg_notice + (strbrk "Hello again " ++ Libnames.pr_reference r)] +END + +VERNAC COMMAND EXTEND TakingConstr CLASSIFIED AS QUERY +| [ "Cmd1" constr(e) ] -> + [ Feedback.msg_notice (strbrk "Cmd1 parsed something") ] +END diff --git a/tuto1/src/tuto1_plugin.mlpack b/tuto1/src/tuto1_plugin.mlpack new file mode 100644 index 0000000000..3b46ea79bf --- /dev/null +++ b/tuto1/src/tuto1_plugin.mlpack @@ -0,0 +1 @@ +G_tuto1
\ No newline at end of file |