Commit e4467110 authored by Raphael Cauderlier's avatar Raphael Cauderlier

Merge branch 'master' of git.lsv.fr:cauderlier/dktactics

parents c362b55b 2d86c509
......@@ -2,3 +2,4 @@
**/*.dko
**/*.dk.depend
dktactics
\#*
\ No newline at end of file
......@@ -117,9 +117,12 @@ done
# Ensures that the file ".config_vars" exists and is empty
echo > .config_vars &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Meta Sukerujo v2.6" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Sukerujo v2.6" &&
(find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.6.0" ||
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti devel") &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" ""
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti 0.1" &&
#find_and_check_binary "skcheck" ".native" "SKCHECK" "-version" "Sukerujo v2.6" &&
#find_and_check_binary "skmeta" ".native" "SKMETA" "-version" "Sukerujo v2.6" &&
if $CONFLUENCE_CHECKING
then
......
......@@ -6,6 +6,7 @@ DKS = $(DKMS:.dkm=.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol
DKMETA_OPTIONS = -I ../fol -I ../meta -nl
DKDEP_OPTIONS = -I ../fol -I ../meta
all: $(DKOS)
......@@ -22,7 +23,7 @@ all: $(DKOS)
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dkm
$(DKDEP) $< | sed "s/\.dkm/\.dk/" > $@
$(DKDEP) $(DKDEP_OPTIONS) $< | sed "s/\.dkm/\.dk/" > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
......
......@@ -10,6 +10,7 @@ endif
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS =
DKDEP_OPTIONS =
all: $(DKOS)
......@@ -24,7 +25,7 @@ builtins.dk.depend: builtins.dk
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
$(DKDEP) $(DKDEP_OPTIONS) $< > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
......
......@@ -4,6 +4,7 @@ include ../.config_vars
DKS = $(wildcard *.dk)
DKOS = $(DKS:.dk=.dko)
DKCHECK_OPTIONS = -I ../fol -nl
DKDEP_OPTIONS = -I ../fol
all: $(DKOS)
......@@ -17,7 +18,7 @@ all: $(DKOS)
# foo.dk.depend lists the modules foo depends on
%.dk.depend: %.dk
$(DKDEP) $< > $@
$(DKDEP) $(DKDEP_OPTIONS) $< > $@
DKDEPENDS = $(DKS:.dk=.dk.depend)
-include $(DKDEPENDS)
......
......@@ -49,12 +49,12 @@ def mintro_proof : A : prop ->
(proof A -> mtactic B) ->
mtactic (imp A B).
[A,B,b] mintro_term A B (x => mret (B x) (b x))
[A,B,b] mintro_term A (x => B x) (x => mret (B x) (b x))
-->
mret (all A B) (fol.all_intro A B (x : term A => b x))
[A,B,e] mintro_term A B (x => mraise (B x) e)
mret (all A (x => B x)) (fol.all_intro A (x => B x) (x : term A => b x))
[A,B,e] mintro_term A (x => B x) (x => mraise (B x) e)
-->
mraise (all A B) e.
mraise (all A (x => B x)) e.
[A,B,b] mintro_proof A B (x => mret B (b x))
-->
mret (imp A B) (fol.imp_intro A B (x : proof A => b x))
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment