Commit 2d86c509 authored by Raphael CAUDERLIER's avatar Raphael CAUDERLIER

Merge branch 'compatibility-2.6' into 'master'

compatibility with Dedukti 2.6

See merge request !1
parents 8105adfe d8bb5c6d
......@@ -2,3 +2,4 @@
*/*.dko
*/*.dk.depend
dktactics
\#*
\ No newline at end of file
......@@ -117,9 +117,10 @@ done
# Ensures that the file ".config_vars" exists and is empty
echo > .config_vars &&
find_and_check_binary "dkcheck" ".native" "DKCHECK" "-version" "Dedukti v2.5.1" &&
find_and_check_binary "dkdep" ".native" "DKDEP" "" "" &&
find_and_check_binary "dkmeta" ".native" "DKMETA" "-version" "Meta Dedukti v2.5.1" &&
(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" &&
......
......@@ -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)
......@@ -18,7 +19,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)
......
......@@ -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))
......
......@@ -224,6 +224,7 @@ b : function.
x : term A.
y : term A.
(;
#SNF unify (unify_cons A x (fun_apply a) unify_nil).
#SNF unify (unify_cons A (fun_apply a) x unify_nil).
#SNF unify' (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply a) unify_nil).
......@@ -232,3 +233,4 @@ y : term A.
#SNF unify (unify_cons A x y unify_nil).
#SNF unify (unify_cons A (fun_apply f x (fun_apply a)) (fun_apply f (fun_apply a) y) unify_nil).
#SNF unify' (unify_cons A (fun_apply f (fun_apply b) y) (fun_apply f y (fun_apply a)) unify_nil).
;)
\ No newline at end of file
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